Monthly Archives: March 2012
A direct proof of Hedberg’s theorem
In his article published 1998, Michael Hedberg has shown that a type with decidable equality also features the uniqueness of identity proofs property. Reading through Nils Anders Danielsson’s Agda formalization, I noticed that the statement “A has decidable equality”, i.e. … Continue reading
Posted in Code
5 Comments
Modeling Univalence in Inverse Diagrams
I have just posted the following preprint, which presents new set-theoretic models of univalence in categories of simplicial diagrams over inverse categories (or, more generally, diagrams over inverse categories starting from any existing model of univalence). The univalence axiom for … Continue reading
Posted in Models, Paper, Univalence
5 Comments
Homotopy Type Theory 