Posted in

Speaker:

Eric Finster
Date:

Wed, 10/02/2016 - 16:30 - 18:00
Location:

MPIM Lecture Hall
Parent event:

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

Curien, but here equipped with a direct higher categorical

interpretation.

© MPI f. Mathematik, Bonn | Impressum & Datenschutz |