UF IAS 2012 Archive Notes

Notes from the final organizational meeting. Fri April 12th.

1. Admin wiki (Dan L will investigate a new infrastructure) Univalent google group will be move to HoTT Book: F.Freeze Sun 11:59 PM, Debugging until: End of May

Please send your IAS reports to Steve who will put them on the wiki.

1. Coq/agda Formalizing the book (Andrej) New Proof Assistant (CMU, IAS, Gothenburg, Ljubljana)

3 Upcoming Meetings:

Coq workshop, Types, AIM, Possible: Dagstuhl, Oberwolfach, Shonan, Leiden, Luminy

Workshops: LICS, CPP, TLCA, CSL, ITP, TYPES, POPL, ICFP, DTP, LFMTP, MSFP MFPS, AMS, ASL, CT13, OctoberFest, PSSL, Union College, MAP

journals: BSL, JSL, RSL, JFR, LMCS, TOCL, APAL, LMCS, TCS, JFP, MSCS, MPCPS, TAC

Open problems:

• Two left fromOberwolfach:
• Simplicial types
• Does there exist a univalent (weakly universal Kan) fibration in the category of simplicial objects in an arbitrary topos?
• Homotopy theory
• Use impredicative polymorphism to justify HITs
• Use HITs to avoid impredicativity, choice
• Ordinal analysis for HoTT
• What the elementary set theory of V (in particular REA, Strong Collection).
• Give a predicative foundation for HITs, UA
• Closure under gluing, sheaves, realizability, …
• Are n-spheres are oo-truncated
• Prove that S2 is not an n-type
• Syntax of HITs
• Universal HIT (like W-type)
• Pattern matching for HITs without K
• Integration of UA with constructive analysis
• Relate weak oo-groupoids with ML complexes
• Elementary theory of higher toposes, aligning higher toposes and HoTT
• Does the global the global section: HoTT -> oo-groupoids (Kan sSet or globular) preserve finite co-lims, S^n, …
• Verifying computational homotopy theory
• Directed HoTT
• Computational interpretation, specifically for pi4(S3). Compute the Brunerie number (2?).
• Semantics of strict resizing
• Semantics for HIIT, HIRT,
• parametricity and UA
• oo-groupoids internal to HoTT
• Bott periocidy in HoTT,
• Cohomology, CAT (Kenzo), Spanier’s book
• Synthetic stable homotopy theory
• Axiomatize Simplicial Types, following Joyal (generic interval)
• Consequences of gluing: uniformity, forall commutes with disjunction, …
• Prove something new: can we integrate all containers/ polynomial functors.
• Relate operads and containers, via dendrodal sets? synthetically
• HoTT and linear logic
• Derive stronger “elimination rules” for truncations / State conditions for a map to factorize trough a truncation (by giving an appropriate notion of constancy). More precise formulation: Given an n-type B, any type A and a number m. Find, without using truncations, a property that is equivalent to having a map from (the m-truncation of A) into B, or show that it is not possible (it is possible for [n < oo and m = -1], and trivial if n is not larger than m).