Category Archives: Applications

Isomorphism implies equality

Thierry Coquand and I have proved that, for a large class of algebraic structures, isomorphism implies equality (assuming univalence). A class of algebraic structures Structures in this class consist of a type, some operations on this type, and propositional axioms … Continue reading

Posted in Applications, Code, Univalence | 13 Comments

A Simpler Proof that π₁(S¹) is Z

Last year, Mike Shulman proved that π₁(S¹) is Z in Homotopy Type Theory. While trying to understand Mike’s proof, I came up with a simplification that shortens the proof a bunch (100 lines of Agda as compared to 380 lines … Continue reading

Posted in Applications, Higher Inductive Types, Models | 5 Comments

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