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