From a homotopy theorist’s point of view, identity types and their connection to homotopy theory are perfectly natural: they are “path objects” in the category of types. However, from a type theorist’s point of view, they are somewhat more mysterious. In particular, identity types are just one particular inductive family; so what’s special about them that they give us homotopy theory and other inductive families don’t? And specifically, how can it be that we “get out” of identity types more than we inductively “put into them”; i.e. why can there be elements of
Id(x,x) other than
refl, whereas for some other inductive types like
Fin, we can prove that there’s nothing in them other than what we put in?
Dan Licata’s recent post partly answered the second of these questions. He pointed out that instead of an inductive family indexed by $latex Atimes A$, we can regard…
View original post 1,662 more words