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.

2. 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 from Oberwolfach:
  • 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).