Monthly Archives: December 2011
Strong functional extensionality from weak
It’s amazing what you can find in the HoTT repository these days! I was browsing it the other week, looking up something quite different, when I came across a theorem in Funext.v (originally by Voevodsky) which answers, in a surprising … Continue reading
A seminar on HoTT Equivalences
I recorded our local Seminar on foundations in which I talked about the notion of equivalence in HoTT: Hopefully some people will find some use for it. It is pretty slowly going, and it might motivate some of the strange … Continue reading
Localization as an Inductive Definition
I’ve been talking a lot about reflective subcategories (or more precisely, reflective subfibrations) in type theory lately (here and here and here), so I started to wonder about general ways to construct them inside type theory. There are some simple … Continue reading
Modeling Univalence in Subtoposes
In my recent post at the n-Category Café, I described a notion of “higher modality” in type theory, which semantically ought to represent a left-exact-reflective sub–category of an -topos — once we can prove that homotopy type theory has models … Continue reading
HoTT in prose
I have adapted some basic HoTT theorems and proofs to prose form, in an attempt to better understand the results and their proofs. The Coq proof scripts often obscure details of the exposition, like the choice of fibration in an induction tactic, … Continue reading
Homotopy Type Theory 