Univalent Foundations of Mathematics - Program Description

We plan to have four main working groups oriented towards the goals described below. However applications from people with interest in other aspects of mathematics and computer science related to the univalent semantics of type theories will also be considered.

For general information on Univalent Foundations and Homotopy Type Theory
see Homotopy Type Theory website and Vladimir Voevodsky’s homepage .

We plan to have a weekly seminar where each of the groups will be given, on average, one spot per month.

Group 1. Design and implementation of a proof assistant based on a universe polymorphic type system with resizing rules.

Goals: To design a type system fully compatible with the univalent model which has universe polymorphism and resizing rules. To start the process of design and implementation of a proof assistant based on this type system.

Group 2. Computational issues in constructive type theory related to the univalence axiom.

Goals: looking for approaches to the proof of the "main computational conjecture" of the univalent approach with a special focus on looking for practical algorithms for automatic construction of fully constructive terms from terms build with the help of extensionality axioms.

Group 3. Formalization of advanced homotopy-theoretic structures in constructive type theory.

Goals: looking for approaches to formalize higher coherence structures (simplicial types, H-types, $n-1$-categories and $n-1$-functors etc.). Looking for possible syntax and computation rules for higher inductive definitions. Looking for the constructions of elements in homotopy groups of spheres as mappings between the corresponding loop "functors".

Group 4. Relation of constructive type theory to set-theoretic foundations.

Goals: formalizations of type theories and known constructions of their models in ZFC and related theories. Looking for new models of constructive type theories, especially for non-standard models of the univalence axiom.