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

Abstracts

Program

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 *set-theoretic* setting, the relationship between those concepts is well-known. 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 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 formalizations.

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

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)