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 |