Skip to main content

Fibration categories, the propositional J rule and setoids

Posted in
Speaker: 
Benno van den Berg
Datum: 
Don, 11/02/2016 - 13:30 - 15:00
Location: 
MPIM Lecture Hall

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).

This talk starts from another link: in homotopy theory a well-known
weakening of the notion of a Quillen model structure is that of a category
of fibrant objects, due to Kenneth Brown. A slight variation of this
notion, which I will call a fibration category, corresponds to a natural
weaking of the rule for the identity type, where we ask for the computation
rule for J to hold only in a propositional form. Indeed, this weakening has
been considered by Coquand and collaborators in their attempt to build
constructive models of homotopy type theory. Ignoring the coherence
problems again, we can say that fibration categories provide a sound and
completeness semantics for these weak identity types.

In constructive mathematics one often avoids taking quotients; instead, one
considers sets together with an arbitrary equivalence relation. In type
theory such an object is called a setoid. In this talk I will show that the
category of setoids can be seen as a two-step construction, where one first
builds a new fibration category out of an old one and then takes the
homotopy category. It turns out that the intermediate fibration category
has interesting properties: for example, it satisfies functional
extensionality even when the original one does not.

If time permits, I also plan to talk about algebraic set theory and models
of Aczel's constructive set theory CZF from weak universes, also in the
context of fibration categories.

(joint work with Ieke Moerdijk)

© MPI f. Mathematik, Bonn Impressum & Datenschutz
-A A +A