[FOM] Why we need a type-theoretic foundation

[Joe Shipman]

David, I see that MorTT has many of the advantages of HoTT while being based on classical rather than constructive logic. 

Another useful feature is that the purely mathematical difficulties related to homotopy theory are no longer involved with the foundation of mathematics.

My question is whether those mathematical difficulties are worth eliminating. In particular, does HoTT make homotopy theory itself, considering the results that topologists and algebraists care about, much easier?

-- JS

Sent from my iPhone

> On Jan 8, 2016, at 6:58 AM, David McAllester <mcallester at ttic.edu> wrote:
> 
> I have just posted what I believe is the final version of a paper on "morphoid type theory" (MorTT).  MorTT is a type-theoretic foundation of mathematics that includes a treatment of isomorphism but that differs form HoTT in that MorTT extends classical predicate calculus rather than constructive type theory.  MorTT does not involve propositions-as-types, path induction, squashing or higher order isomorphisms. I have also written a blog post on why we need a type-theoretic foundation.  Discussion is welcome.
> 
> David McAllester
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160108/d5dd8be7/attachment.html>