Re: [HoTT] Re: Where is the problem with initiality?

[Alexander Kurz <axh...@gmail.com>]

> On 30 May 2018, at 10:37, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote:
> 
> On 30/05/2018, 10:33, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote:
> 
>    That categorical syntax and ordinary syntax are isomorphic is just a
>    purely syntactic result allowing one to replace correct algebraic
>    syntax by one more accessible for the human mind.
> 
> For the human mind accustomed to the separation of collections and predicates as present in conventional Mathematics.

I think the problem is not just one of being accustomed or not. 

It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed. 

If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved. 

Alexander

> 
> 
> 
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.