Alternatively have a look at the program.

## Dependent Type Theories

Modern dependent type theories exist mostly in the form of computer programs. As such they are objects of the physical reality more than they are objects of the mathematical one. For three decades the world of type theories was relatively calm - innovation was largely occurring in the layers of programming above the type theories leading to proof assistants with more and more sophisticated systems for notation, implicit arguments and tactics.

## Internal languages of higher categories

Homotopy Type Theory is often referred to informally as the internal

language of higher category theory. This slogan can be made precise, and I

will state and explain the corresponding conjectures. Afterwards, I will

report on the progress towards proving these conjectures.

## 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

## Dependent Type Theories

## Fibration categories, the propositional J rule and setoids

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

## Eine Wanderung durch Rainer Vogt's mathematisches Schaffen (A journey through Rainer Vogt's mathematical work) - MPI-Oberseminar jointly with the Workshop on Homotopy Type Theory -

Rainer Vogt left us last August. With Mike Boardman and Peter

May he invented operads (in particular the little cubes operad) and used

them to conceptualise the notions of homotopy coherence and of homotopy

invariance. Both are fundamental in the study of higher structures. I'll

try to highlight some aspects of Rainer Vogt's work by looking more

closely at several of his articles.

## Homotopy theory of type theories

## Dependent Type Theories

## Cubical sets as a classifying topos

We will provide a description of the cubical model based on the

internal logic of the topos of cubical sets. To be precise, we will

show what this topos classifies and how this helps us to simplify the

presentation of the model. Specifically, this will allow us to

describe the geometrical realization as a geometric morphism from

Johnstone’s topological topos.

This work is the basis for a semantics of an extension of cubical type

theory with guarded dependent types. The latter part is joint work

within the logic and semantics group in Aarhus.

## The quaternionic Hopf fibration in HoTT via a modified Cayley-Dickson construction

One of the open problems in the development of synthetic homotopy

theory in homotopy type theory has been the construction of the

quaternionic and octonionic Hopf fibrations, arising from the H-space

structures on the three- and seven-sphere, respectively. Classically,

we can get these by considering the unit spheres in the quaternion and

octonion algebras, which we in turn can define using the

Cayley-Dickson construction. Here, we give a modified version of this

construction that works directly with the unit spheres, and in the

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