Higher categories with families

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
Curien, but here equipped with a direct higher categorical
interpretation.