Skip to main content

Abstracts for Workshop on Homotopy Type Theory

Alternatively have a look at the program.

Dependent Type Theories

Posted in
Speaker: 
Vladimir Voevodsky
Affiliation: 
IAS/MPIM
Date: 
Wed, 2016-02-10 10:00 - 11:00
Location: 
MPIM Lecture Hall

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

Posted in
Speaker: 
Chris Kapulkin
Date: 
Wed, 2016-02-10 14:30 - 16:00
Location: 
MPIM Lecture Hall

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

Posted in
Speaker: 
Eric Finster
Date: 
Wed, 2016-02-10 16:30 - 18:00
Location: 
MPIM Lecture Hall

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

Posted in
Speaker: 
Vladimir Voevodsky
Affiliation: 
IAS/MPIM
Date: 
Thu, 2016-02-11 10:00 - 11:00
Location: 
MPIM Lecture Hall

Fibration categories, the propositional J rule and setoids

Posted in
Speaker: 
Benno van den Berg
Date: 
Thu, 2016-02-11 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).

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 -

Posted in
Speaker: 
Clemens Berger
Date: 
Thu, 2016-02-11 15:00 - 16:00
Location: 
MPIM Lecture Hall

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

Posted in
Speaker: 
Peter Lumsdaine
Date: 
Thu, 2016-02-11 16:30 - 18:00
Location: 
MPIM Lecture Hall

Dependent Type Theories

Posted in
Speaker: 
Vladimir Voevodsky
Affiliation: 
IAS/MPIM
Date: 
Fri, 2016-02-12 10:00 - 11:00
Location: 
MPIM Lecture Hall

Cubical sets as a classifying topos

Posted in
Speaker: 
Bas Spitters
Date: 
Fri, 2016-02-12 13:30 - 15:00
Location: 
MPIM Lecture Hall

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

Posted in
Speaker: 
Ulrik Buchholtz
Date: 
Fri, 2016-02-12 15:30 - 17:00
Location: 
MPIM Lecture Hall

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
-A A +A