Skip to main content
Get your brand new Wikispaces Classroom now
and do "back to school" in style.
Pages and Files
Categorical Semantics WG
Coq for UF
Coq Working Group
Formalized Homotopy Theory
Higher Inductive Types
Homotopy Type System
how to add a plugin
IAS program participants
Informal Type Theory
Math in HoTT
Modal type theory
Notation and terminology
Add "All Pages"
Notes from the final organizational meeting. Fri April 12th.
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.
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
Two left from
Does there exist a univalent (weakly universal Kan) fibration in the category of simplicial objects in an arbitrary topos?
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
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).
help on how to format text
Turn off "Getting Started"