Workshop on Homotopy Type Theory / Univalent Foundations
June 29–30, 2015, Warsaw, Poland
Collocated with RDP/TRA/TLCA 2015.
Overview
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, HoTTAgda…), what logical features are convenient for the formalisation of “homotopical mathematics”, and how to make formalisation in HoTT/UF accessible and practical for mathematicians.
Abstracts
You can download abstracts of contributed talks here.
Program
 Monday 29
 9:15–10:15 RTA plenary
 10h1510h45: coffee break
 10h4511h45: invited talk, Matthieu Sozeau, Coq Support for HoTT
 11h4512h45: invited talk, Assia Mahboubi, Coq Libraries for
HoTT slides.
 12h4514h00: lunch
 14h0014h45: contributed talk
 Simon Huber, Cyril Cohen, Thierry Coquand and Anders
Mörtberg. A Cubical Type Theory slides
 14h4515h30: round table
 15h3016h: coffee break
 16h0017h30: contributed talks
 Hugo Herbelin. An Inductive DependentlyTyped Construction of
Simplicial Sets and of similar Presheaves over a Reedy Category
slides
 Kevin Quirin. LawvereTierney 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
 Tuesday 30
 9:00–10:00 RTA plenary
 10h10h30 : coffee break
 10h3011h30: invited talk, Thorsten Altenkirsh, Univalence for Dummies?slides
 11h3012h30: contributed talks,
 Christian Sattler. Ordinary and Indexed WTypes
 Nicolai Kraus. Eliminating out of Truncations slides
 12h3014h: lunch
 14h15h30: RDP plenary session
 14h0015h00: Vladimir Voevodsky, From Syntax
to Semantics of Dependent Type Theories  formalized slides
 1515h30: Florence Clerc, Samuel Mimram. Presenting Categories Modulo a Rewriting System
 15h3016h00: coffee break
 16h0017h00: invited talk, Benedikt Ahrens, Models of Type
Theory in Univalent Mathematics slides
 17h0017h30: contributed talk,
 Martin Escardo and Thierry Coquand. The Geometry of
Constancy slides and
code
 17h30open: discussions
Invited Speakers

Benedikt Ahrens,
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
substitution.
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 *settheoretic* setting, the relationship between those concepts is
wellknown.
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
library.
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
audience.
Assia Mahboubi, Coq Libraries for HoTT
Many investigations in Homotopy Type Theory and Univalent Foundations
have been simultaneously formalized and machinechecked in
preexisting (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
formalizations.

Matthieu Sozeau, Coq support for HoTT
In this tutorial I will present upandcoming, 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 workinprogress update of the Equations
package, enables full dependent patternmatching syntax for writing
programs, using general wellfounded recursion and making use of
the hlevel information on types to compile patternmatching down
to pure, axiomfree 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 roundtable 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.
Submissions
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.
Organisers
 Peter LeFanu Lumsdaine,
p.l.lumsdaine at gmail.com
(Stockholm University)
 Nicolas Tabareau,
nicolas.tabareau at inria.fr
(Inria, Rennes)
Program Committee
 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