Category Archives: Applications
Impredicative Encodings of Inductive Types in HoTT
I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here. Known impredicative encodings of various inductive types in System F, such as the type of natural numbers do not … Continue reading
HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics
SQL is the lingua franca for retrieving structured data. Existing semantics for SQL, however, either do not model crucial features of the language (e.g., relational algebra lacks bag semantics, correlated subqueries, and aggregation), or make it hard to formally reason … Continue reading
Combinatorial Species and Finite Sets in HoTT
(Post by Brent Yorgey) My dissertation was on the topic of combinatorial species, and specifically on the idea of using species as a foundation for thinking about generalized notions of algebraic data types. (Species are sort of dual to containers; … Continue reading
Real-cohesive homotopy type theory
Two new papers have recently appeared online: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory by me, and Adjoint logic with a 2-category of modes, by Dan Licata with a bit of help from me. Both of them have fairly … Continue reading
Higher Lenses
Lenses are a very powerful and practically useful functional construct. They represent “first class” fields for a data structure. Lenses arose in work on bidirectional programming (for example, in Boomerang), and in Haskell, people have given many different definitions of … Continue reading
Eilenberg-MacLane Spaces in HoTT
For those of you who have been waiting with bated breath to find out what happened to your favorite characters after the end of Chapter 8 of the HoTT book, there is now a new installment: Eilenberg-MacLane Spaces in Homotopy Type Theory Dan … Continue reading
Homotopy Theory in Homotopy Type Theory: Introduction
Many of us working on homotopy type theory believe that it will be a better framework for doing math, and in particular computer-checked math, than set theory or classical higher-order logic or non-univalent type theory. One reason we believe this … Continue reading
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
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
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
Homotopy Type Theory 