# Re: Homotopy Type Theory

```Physical computation was discovered by nature 4000 Million years BT
(Before Turing) . And even before.```
```
2014/1/12, Bruno Marchal <marc...@ulb.ac.be>:
>
> On 11 Jan 2014, at 22:41, Alberto G. Corona wrote:
>
>> By the way, what about if you find a mathematical theory that show
>> that:
>>
>> computer programs and matematical proofs  are no longer something out
>> of math,
>
> This is non sense. Computer programs have born in math.
>
>
>
>
>> but mathematical structures and both are essentially the same
>> thing:
>
> The computable is purely mathematical since birth (excepting Babbage,
> but even Babbage discovered it was mathematical at the end of his
> life, arguably, from a work due to Jacques Lafitte).
> But the mathematical, classically conceived,  is *much* larger than
> the computable.
> N^N is not enumerable. the computable restriction of N^N is enumerable.
>
>
>
>> both are paths from premises to conclussion in a  space with
>> topological properties
>
> That does not make them identical.
>
>
>
>>
>> And the theory stablish topological relations between these paths so
>> that proofs and computer algorithms are classified according with
>> these relations.
>
> You might study the book by Szabo, on the category approach on the
> algebra of proofs.
> But proofs and computations are not equivalent concept at all. There
> is a Church's thesis for computability, not for provability and
> definability which are machines or theories dependent.
>
>
>
>>
>> That is homotopy type theory.
>>
>> http://homotopytypetheory.org/
>>
>> I´m starting to learn something about it, It is based on type theory,
>> category theory and topology.
>
> That is very interesting, and category provides nice model for
> constructive subpart of the computable, like typed lambda calculus.
> But category becomes very hard on the complete algebra of computation.
> the partial nature of the fiunctions involved makes hard to even
> compute a co-product.
>
>
>
>> The book introduction is nice (HOTT link
>> at the bottom of the page). It seems to be a foundation of computer
>> science and math that unify both at a higher level, since proofs and
>> programs become legitimate mathematical structures
>
> They are since Church thesis. That is all what computability or
> recursion theory is all about.
> The rest is semantics of languages, more useful in computing theory
> than in computability theory, which is born, I insist, before we
> implement physical computer. The computer have been disocvered by
> mathematicians, in mathematics, indeed, in arithmetic. Those notions
> are born mathematical.
>
> Only later, some physicists have tried to get, without any success, a
> notion of physical computation.
>
>>
>> The book:
>>
>> http://homotopytypetheory.org/2013/06/20/the-hott-book/
>
> Guiseppe Longo wrote also nice book on that subject.  It is a vast
> field, but Gödel made "proof" into arithmetical objects well before,
> as the notion of computations will follow soon after (if not before if
> we take Post's unpublished anticipation into account).
>
>
> Bruno
>
>
>
>>
>> --
>> Alberto.
>>
>> --
>> You received this message because you are subscribed to the Google
>> Groups "Everything List" group.
>> To unsubscribe from this group and stop receiving emails from it,
>> send an email to everything-list+unsubscr...@googlegroups.com.
>> To post to this group, send email to everything-list@googlegroups.com.
>> Visit this group at http://groups.google.com/group/everything-list.
>> For more options, visit https://groups.google.com/groups/opt_out.
>
> http://iridia.ulb.ac.be/~marchal/
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Everything List" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> To post to this group, send email to everything-list@googlegroups.com.
> Visit this group at http://groups.google.com/group/everything-list.
> For more options, visit https://groups.google.com/groups/opt_out.
>

--
Alberto.

--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email