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

[Jon Sterling <j...@jonmsterling.com>]

I fear that this veers off topic---but let me say that this is hardly a serious problem for structural / typed foundations, considering the fact that you can always embed an untyped mathematical universe into a typed one in an easy way (for instance, using Aczel's interpretation of constructive set theory into type theory), whereas it is much harder to move in the other direction without inheriting the pathologies of set theory.

With that said, maybe we can get back to the original question. Where really is the problem with initiality? As Thomas said, the problem surely does not at all lie in the difference between "human syntax" and syntax based on categorical gadgets (it's easy to see that these are the same). Returning to Thomas's email about M_a and M_s (lindenbaum-tarski model), it sounds as if the problem has almost nothing to do with initiality at all, if the hard part is really to show that M_s is a model at all.

Am I misunderstanding Thomas's email?


On Wed, May 30, 2018, at 3:53 AM, Alexander Kurz wrote:
> 
> 
> > 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.
> 
> -- 
> 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.