Higher inductive-recursive univalence and type-directed definitions

Homotopy Type Theory

In chapter 2 of the HoTT book, we prove theorems (or, in a couple of cases, assert axioms) characterizing the equality types of all the standard type formers. For instance, we have

$latex ((a,b) =_{Atimes B} (a’,b’)) simeq (a=_A a’) times (b=_B b’) $


$latex (f =_{Ato B} g) simeq prod_{x:A} f(x) =_B g(x) $

(that’s function extensionality) and

$latex (A =_{mathcal{U}} B) simeq (A simeq B) $

(that’s univalence). However, it’s a bit annoying that these are only equivalences (or, by univalence, propositional equalities). For one thing, it means we have to pass back and forth across them explicitly, which is tedious and messy. It may also seem intuitively as though the right-hand sides ought to be the definitions of the equality types on the left. What can be done?

View original post 2,209 more words

This entry was posted in Computer science, homotopy type theory, Philosophie. Bookmark the permalink.