# Re: Homotopy Type Theory

```2014/1/12, Bruno Marchal <marc...@ulb.ac.be>:
>
> On 12 Jan 2014, at 02:41, Alberto G. Corona wrote:
>
>> But the proofs where not studied before as mathematical structures.
>> Godel and any mathematician did profs, but proofs where
>> meta-mathematical, in the sense that they were not mathematical
>> objects,
>
> No, that is not true at all, and meaningless. Gödel did arithmetize
> meta-arithmetic. His whole proofs is based on this.```
```
That is not the same than study proofs themselves inside math than
reduce them to arithmetic or set theory. Moreover, what Godel did was
called meta-mathematics AFAIK
>
>
>
>
>
>> although they could be formalized in a language.
>
> And then translated in math, even arithmetic.
>
>
>
>> The same
>> happened with the notion of equality and equivalence etc That are
>> defined in a fuzzy or ad-hoc way. HOTT study how equal are two things
>> depending on the path from the one to the other, that is , what
>> topology has the proof of equality between the two.
>
> That is interesting work, but it is a restriction on some typed or
> constructive approach.
> It does not make things more mathematical, as it was elementary
> arithmetic from the start, as Gödel and the sequel have proven.
>
> Note that, computation can be seen as a particular case of proof, and
> proof can be seen as a particular case of computations, but those
> concept are quite different and obeys to quite different mathematics.
> That happens often. You can see a function as particular case of a
> relation (functional relation), and you can see a relation as a
> particular case of a function (by the characteristic function), but
> relation and function are not the same notion.
>
> Any way, both computation and proof are mathematical object in
> computer science and mathematical logic, since the start.
>
> Bruno
>
>
>
>>
>> 2014/1/11, LizR <lizj...@gmail.com>:
>>> That sounds like (some of) what Bruno talks about. The computer
>>> programme
>>> known as the UD (and its trace) are "in maths". (And didn't Godel
>>> make
>>> proofs paths of maths?)
>>>
>>>
>>> On 12 January 2014 10:41, Alberto G. Corona <agocor...@gmail.com>
>>> 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, but mathematical structures and both are essentially the
>>>> same
>>>> thing: both are paths from premises to conclussion in a  space with
>>>> topological properties
>>>>
>>>> And the theory stablish topological relations between these paths so
>>>> that proofs and computer algorithms are classified according with
>>>> these relations.
>>>>
>>>> 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. The book introduction is nice (HOTT
>>>> 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
>>>>
>>>> The book:
>>>>
>>>> http://homotopytypetheory.org/2013/06/20/the-hott-book/
>>>>
>>>> --
>>>> 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.
>>>>
>>>
>>> --
>>> 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-
>>> 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 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
> 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.
>

--
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