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)

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

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: