Abstracts for Workshop on Homotopy Type Theory

Categories with families are an extremely useful reformulation of the
syntax of dependent type theory in categorical terms. We show in this
talk how using (a slight modification of) the Baez-Dolan definition of
opetopic higher category, one can describe the notion of a "higher
category with families" in completely a elementary, that is, syntactic
way. The resulting structure may be regarded as a weakened version of
type theory in which the conversion rule is rendered proof-relevant
and is thus similar in spirit to the explicit substitution calculus of

Homotopy type theory is based on the fact that similar categorical
structures appear in both type theory and homotopy theory. Paths and higher
homotopies give every topological space the structure of an oo-groupoid,
and so does the identity type in type theory. Quillen model categories are
the most common abstract framework for homotopy theory, but also give rise
to models of the identity type (modulo coherence problems relating to
substitution).

We will provide a description of the cubical model based on the
internal logic of the topos of cubical sets. To be precise, we will
show what this topos classifies and how this helps us to simplify the
presentation of the model. Specifically, this will allow us to
describe the geometrical realization as a geometric morphism from
Johnstone’s topological topos.

This work is the basis for a semantics of an extension of cubical type
theory with guarded dependent types. The latter part is joint work
within the logic and semantics group in Aarhus.