Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Vladimir Voevodsky <vlad...@ias.edu>]

[-- Attachment #1.1: Type: text/plain, Size: 2776 bytes --]

The original approach to the UF in 2005-2006 used homotopy lambda calculus, the type theory that I tried to construct, that did not have Martin-Lof identity types. In fact, the idea of having many elements of the identity type in the empty context is against Martin-Lof’s philosophy. MLTT in the form of the CIC just happened to be both implemented in Coq and not inconsistent with the UA opening a way for practical formalization of mathematics in the UF style. This led to the UniMath and a number of HoTT libraries and gave us a great platform for experiment.

However the original philosophy of MLTT and the original philosophy of UF are different and our use of MLTT for UF is in a sense an abuse of the MLTT as Per himself politely mentioned a number of times.

The current work on the development of new type theories led by Bob Harper, Thorsten Altenkirch and Thierry Coquand (and probably others whom I have forgotten to mention) moves us towards a native formal system for the UF but we don’t yet have such a system. We are also isolated from many and many mathematicians who are trying to find a way to express ideas that in my opinion are most naturally expressed in the UF in various theories formulated inside the set theory.

It is, currently, not the best time for the attempts to summarize the theory. We are far having it and I see no other tactic then to move forward slowly and invest into attracting mathematicians to what we do.

Vladimir.





> On Jun 3, 2016, at 2:53 PM, Andrew Polonsky <andrew....@gmail.com> wrote:
> 
> Let me then come to the last of the three questions. What is UTT
> (univalent type theory)? As I conceive it:
> 
>      It is any Martin-Lof type theory that is compatible with the idea
>      that equality/equivalence, as rendered by the identity type, is,
>      in general, structure rather than merely a property.
> 
> I find this definition somewhat puzzling.  Cubicaltt is certainly compatible with the idea that equality is equivalence.  But its path type seems to be a very different concept compared to Martin-Lof identity type.
> 
> What is a Martin-Lof type theory anyway?  Are type systems based on untyped conversion (eg. Coq) Martin-Lof type theories?  Are type theories with a different notion of equality (eg. observational or cubical type theories) also Martin-Lof type theories?
> 
> Andrew
> 
> --
> 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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #1.2: Type: text/html, Size: 4117 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]