Comprehension bicategories

Add to your list(s) Download to your calendar using vCal

• Niels van der Weide, University of Birmingham
• Friday 10 December 2021, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact Paul Levy.

In recent years, many variants of higher dimensional type theory have been studied. Higher dimensional type theory is a form of type theory where the identity type could have elements that are unequal. Among those are a simple type theory which is the internal language for cartesian closed bicategories (studied by Fiore and Saville), directed type theory where the identity types are not symmetric (studied by Licata and Harper and by North), and Martin-Löf type theory with extensionality for identity types of identity types (studied by Garner and by Licata and Harper). A wide variety of techniques have been used to define models of these languages, but a unifying one is missing.

In category theory, comprehension categories provide such a unifying notion. However, they are insufficient to provide interpretations of the mentioned 2-dimensional type theories. That is because some flavors of 2-dimensional type theory have judgments and structural rules that are present in 1-dimensional type theory. For example, Licata and Harper have a judgment for transformations of substitutions and one can also transport along these.

Our goal is to develop a framework that can be used to interpret all these different kinds of type theory. To do so, we develop the notion of a comprehension bicategory, and for that, we need fibrations of bicategories, which have already been defined by Buckley. In this talk, we discuss fibrations of bicategories and we propose a definition of comprehension bicategory. The current material is work in progress with Ahrens and North, and it is being formalized using UniMath.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, SoCS and Zoom (see abstract for link)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.