[FOM] Why we need a type-theoretic foundation

[David McAllester]

I have just posted what I believe is the final version of a paper on
"morphoid type theory" <http://arxiv.org/abs/1407.7274> (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
<https://machinethoughts.wordpress.com/2016/01/01/why-we-need-a-new-foundation-of-mathematics/>
on
why we need a type-theoretic foundation.  Discussion is welcome.

David McAllester <http://ttic.edu/mcallester>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160108/4d1a8bf9/attachment.html>