Monthly Archives: November 2012
On h-Propositional Reflection and Hedberg’s Theorem
Thorsten Altenkirch, Thierry Coquand, Martin Escardo, Nicolai Kraus Overview Hedberg’s theorem states that decidable equality of a type implies that the type is an h-set, meaning that it has unique equality proofs. We describe how the assumption can be weakened. … Continue reading
On Heterogeneous Equality
(guest post by Jesse McKeown) A short narative of a brief confusion, leading to yet-another-reason-to-think-about-univalence, after which the Author exposes his vaguer thinking to derision. The Back-story In the comments to Abstract Types with Isomorphic Types, Dan Licata mentioned O(bservational)TT, … Continue reading
All Modalities are HITs
Last Friday at IAS, Guillaume Brunerie presented a very nice proof that for all . I hope he will write it up and blog about it himself; I want to talk instead about a question regarding modalities that was raised … Continue reading
Abstract Types with Isomorphic Types
Here’s a cute little example of programming in HoTT that I worked out for a recent talk. Abstract Types One of the main ideas used to structure large programs is abstract types. You give a specification for a component, and … Continue reading
Homotopy Type Theory 