Category Archives: Foundations
A type theoretical Yoneda lemma
In this blog post I would like to approach dependendent types from a presheaf point of view. This allows us to take the theory of presheaves as an inspiration for results in homotopy type theory. The first result from this … Continue reading
Inductive Types in HoTT
With all the excitement about higher inductive types (e.g. here and here), it seems worthwhile to work out the theory of conventional (lower?) inductive types in HoTT. That’s what Nicola Gambino, Kristina Sojakova and I have done, as we report … 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
Canonicity for 2-Dimensional Type Theory
A consequence of the univalence axiom is that isomorphic types are equivalent (propositionally equal), and therefore interchangable in any context (by the identity eliminaiton rule J). Type isomorphisms arise frequently in dependently typed programming, where types are often refined to … Continue reading
Higher Inductive Types via Impredicative Polymorphism
The proof assistant Coq is based on a formal system called the “Predicative Calculus of (Co)Inductive Constructions” (pCiC). But before pCiC, there was the “Calculus of Constructions” (CoC), in which inductive types were not a basic object, but could be … Continue reading
Running Circles Around (In) Your Proof Assistant; or, Quotients that Compute
Higher-dimensional inductive types are an idea that many people have been kicking around lately; for example, in An Interval Type Implies Function Extensionality. The basic idea is that you define a type by specifying both what it’s elements are (as … Continue reading
Oberwolfach Report
Richard Garner has now completed and posted the report from the Oberwolfach meeting.
Just Kidding: Understanding Identity Elimination in Homotopy Type Theory
Several current proof assistants, such as Agda and Epigram, provide uniqueness of identity proofs (UIP): any two proofs of the same propositional equality are themselves propositionally equal. Homotopy type theory generalizes this picture to account for higher-dimensional types, where UIP … Continue reading
An Interval Type Implies Function Extensionality
One of the most important spaces in homotopy theory is the interval (be it the topological interval or the simplicial interval ). Thus, it is natural to ask whether there is, or can be, an “interval type” in homotopy type … Continue reading
Constructive Validity
(This is intended to complement Mike Shulman’s nCat Cafe posting HoTT, II.) The Propositions-as-Types conception of Martin-Löf type theory leads to a system of logic that is different from both classical and intuitionistic logic with respect to the statements that hold … Continue reading
Homotopy Type Theory, II | The n-Category Café
Mike Shulman has another great posting on HoTT over at the n-Cat Cafe’. It starts out like this: Homotopy Type Theory, II — Posted by Mike Shulman … Last time we talked about the correspondence between the syntax of intensional … Continue reading
