[TYPES/announce] Univalent Foundations Program - important update.

[Vladimir Voevodsky]

Dear All,

it is only now that we have fully realized that the plan for the next year program at the IAS as it is stated in the web 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 .
> In connection with the activities of Group 1 there will probably be a series of presentations based on the "Univalent Foundations" library as it will be by that time.
> For all other purposes we plan to have a weekly seminar where each of the groups will be given, on average, one spot per month.

> Group 1. Practical formalization of set-level mathematics in Coq based on the univalent approach.
> Goals: developing skills for collective work on libraries of formalized mathematics, locating the points of "tension" between constructive and non-constructive approaches especially in the formalization of analysis, creating libraries for future use.

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

must be changed.

We reason as follows. The ultimate goal of the univalent program is to make formalized and computer verified proofs a standard in pure and eventually in applied mathematics. A necessary intermediate goal is to have a proof assistant based on a type system which is compatible with the univalent model and implements resizing rules.  

Because of this fact we decided put as Group 1 a group which will start working on a type system and a proof assistant with required properties. 

It is a very serious change but we feel strongly that it is necessary. 

The further discussion related to this issue will be only posted to HOTT ( homotopytypetheory at googlegroups.com ) so please subscribe to it if you would like to follow the discussion and/or participate in the project itself. 

Steve Awodey, Thierry Coquand and Vladimir Voevodsky (organizers of the Univalent Foundations program).


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20120530/6ded5047/attachment.html>