Workshop on Homotopy Type Theory / Univalent Foundations
June 29–30, 2015, Warsaw, Poland
Collocated with RDP/TRA/TLCA 2015.
Homotopy Type Theory/Univalent Foundations is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, informed by ideas and tools from abstract homotopy theory.
One practical goal of the programme is to facilitate computer formalisation of mathematics in such logical systems.
We aim to focus on that aspect: bringing together researchers on formalisation in UF/HoTT to discuss the various established and experimental proof assistants for it, the different libraries available (HoTT Coq, Unimath, HoTT-Agda…), what logical features are convenient for the formalisation of “homotopical mathematics”, and how to make formalisation in HoTT/UF accessible and practical for mathematicians.
You can download abstracts of contributed talks here.
- Monday 29
- 9:15–10:15 RTA plenary
- 10h15-10h45: coffee break
- 10h45-11h45: invited talk, Matthieu Sozeau, Coq Support for HoTT
- 11h45-12h45: invited talk, Assia Mahboubi, Coq Libraries for
- 12h45-14h00: lunch
- 14h00-14h45: contributed talk
- Simon Huber, Cyril Cohen, Thierry Coquand and Anders
Mörtberg. A Cubical Type Theory slides
- 14h45-15h30: round table
- 15h30-16h: coffee break
- 16h00-17h30: contributed talks
- Hugo Herbelin. An Inductive Dependently-Typed Construction of
Simplicial Sets and of similar Presheaves over a Reedy Category
- Kevin Quirin. Lawvere-Tierney Sheafification in Homotopy
Type Theory slides
- Andreas Nuyts, Jesper Cockx, Dominique Devriese and Frank Piessens.
Towards a Directed HoTT with Four Kinds of Variance slides
14h-15h30: RDP plenary session
- 9:00–10:00 RTA plenary
- 10h-10h30 : coffee break
- 10h30-11h30: invited talk, Thorsten Altenkirsh, Univalence for Dummies?slides
- 11h30-12h30: contributed talks,
- Christian Sattler. Ordinary and Indexed W-Types
- Nicolai Kraus. Eliminating out of Truncations slides
15-15h30: Florence Clerc, Samuel Mimram. Presenting Categories Modulo a Rewriting System
15h30-16h00: coffee break
16h00-17h00: invited talk, Benedikt Ahrens, Models of Type
Theory in Univalent Mathematics slides
17h00-17h30: contributed talk,
- 14h00-15h00: Vladimir Voevodsky, From Syntax
to Semantics of Dependent Type Theories - formalized slides
- Martin Escardo and Thierry Coquand. The Geometry of
Constancy slides and
Models of Type Theory in Univalent Mathematics
The categorical semantics of type theory has been subject of research
since the 1970s.
A model of type theory is usually defined to be a category - modelling
contexts and their morphisms - that is equipped with additional
structure accounting for types and terms, and operations such as
The type theory itself can be given such a structure of a model - in
fact, the inductive structure of type theory entails that it is the
initial such model in a suitable sense.
Various definitions of models as "categories with extra structure" have
been studied, amongst them
- categories with families ;
- categories with attributes ;
- categories with display maps ;
- comprehension categories.
In a *set-theoretic* setting, the relationship between those concepts is
In ongoing work with Peter LeFanu Lumsdaine and Vladimir Voevodsky, we
try to understand the relation between these different notions in
*univalent* mathematics, by exhibiting maps between the different types
of such models and showing which are embeddings, equivalences, and so on.
In this talk I will give an overview of the UniMath library, a library
of univalent mathematics formalized using the proof assistant Coq, and
of our formalization of models of type theory based on the UniMath
Thorsten Altenkirch, Univalence for Dummies?
One of the central principles of Homotopy Type Theory is the
univalence "axiom" which basically states that equivalent types are
equal. But why is this sound? Both the setoid model and the groupoid
model give us a limited form of univalence but how to scale it up?
Are Kan complexes the right answer? Or cubical sets? I would like to
discuss this question and I expect some useful input from the
Assia Mahboubi, Coq Libraries for HoTT
Many investigations in Homotopy Type Theory and Univalent Foundations
have been simultaneously formalized and machine-checked in
pre-existing (like Agda or Coq) or new (like Lean) proof assistants,
possibly customized for this purpose. This results today in rather
larger corpus of formal libraries, that require some care and
maintenance from their authors in order to remain a robust and
extensible socle for further developments. In this lecture we do not
present new formalized results but rather try to illustrate how the
techniques drawn up in the collaborative development of large
libraries like the Mathematical Components can apply to this flavor of
Matthieu Sozeau, Coq support for HoTT
In this tutorial I will present up-and-coming, definitional extensions
for the development of HoTT in Coq. The first, a generalized rewriting
framework working in Type, enables rewriting with equivalences,
relevant identity or any user defined relevant rewriting relation in
any context. The second, a work-in-progress update of the Equations
package, enables full dependent pattern-matching syntax for writing
programs, using general well-founded recursion and making use of
the h-level information on types to compile pattern-matching down
to pure, axiom-free Coq terms. It also provides tools to reason on programs
after the fact without leaking details of the elaboration. In particular
it derives powerful functional elimination principles coming from the
the inductively defined graphs of functions. We will discuss potential
applications and extensions with HITs.
This is joint work with Cyprien Mangin.
Vladimir Voevodsky, From Syntax to Semantics of Dependent Type Theories - formalized
The keystone of the homotopy type theory and univalent foundations is the interpretation of the Calculus of Inductive Constructions into Kan simplicial sets that satisfies the univalence axiom. The detailed description of this interpretation is very complex and requires new level of generality and precision in the theory of syntax and semantics of dependent type theories. I will report on the current state of the program for a rigorous, formalizable approach to the construction of models of complex dependent type theories that I have been working on since 2009.
Format and schedule
The work shop will include invited talks, contributed talks, and a round-table discussion session.
The discussion topic is the state of libraries and documentation for programming in HoTT using Coq and Agda.
We hope to stimulate effort to make the existing resources more accessible, and improve and supplement them where they are lacking, to help new researchers get active in this topic.
For practical details, registration, etc., see the main RDP site.
Abstract submission deadline: April 15, 2015.
Submissions should consist of a title and abstract, in pdf or text format, via EasyChair
Talks on practical formalisation are particularly solicited, but submissions on all UF/HoTT topics are welcome.
- Peter LeFanu Lumsdaine,
p.l.lumsdaine at gmail.com (Stockholm University)
- Nicolas Tabareau,
nicolas.tabareau at inria.fr (Inria, Rennes)
- Benedikt Ahrens (Université Paul Sabatier, Toulouse)
- Steve Awodey (Carnegie Mellon University)
- Eric Finster (École Polytechnique)
- Dan Licata (Wesleyan University)
- Andrew Polonsky (VU University Amsterdam)
- Peter LeFanu Lumsdaine (Stockholm University)
- Nicolas Tabareau (Inria, Rennes)
Last modified: Fri Mar 11 00:32:33 CET 2016