Monthly Archives: March 2011

A Formal Proof that the Higher Fundamental Groups are Abelian

Homotopy type theory (HoTT) will have applications for both computer science and math. On the computer science side, applications include using homotopy type theory’s more general notion of equality to make formal verification of software easier. On the mathematical side, … Continue reading

Posted in Applications | 13 Comments

Constructive Validity

(This is intended to complement Mike Shulman’s nCat Cafe posting HoTT, II.) The Propositions-as-Types conception of Martin-Löf type theory leads to a system of logic that is different from both classical and intuitionistic logic with respect to the statements that hold … Continue reading

Posted in Foundations | 17 Comments

Homotopy Type Theory, II | The n-Category Café

Mike Shulman has another great posting on HoTT over at the n-Cat Cafe’. It starts out like this: Homotopy Type Theory, II — Posted by Mike Shulman … Last time we talked about the correspondence between the syntax of intensional … Continue reading

Posted in Foundations | Leave a comment

Function Extensionality from Univalence

Andrej Bauer and Peter Lumsdaine have worked out a proof of Function Extensionality from Univalence that is somewhat different from Vladimir Voevodsky’s original.  In it, they identify and employ a very useful consequence of Univalence: induction along weak-equivalences.  Andrej has … Continue reading

Posted in Univalence | 6 Comments