Notes

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

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

- 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 , and trivial if n is not larger than m).

Created on April 19, 2018 at 17:16:58
by
Univalent foundations special year 2012