The Book


We have started talking about a collection of notes. More info on the page about The book.

Working group on informal type theory


One of our projects is to present informal versions of various theorems, both verbally and in a written way, and criticize them. These theorems may or may not have yet been proven formally.

For Oct 23 (potentially)

  • pi_1(S^1) = Z (Guillaume B.) (pdf here)
  • Relationships between various kinds of equivalence (Kristina S.)
  • S^1 x S^1 is equivalent to T^2 (Dan L.)

Future proposals

  • Univalence implies function extensionality
  • Properties of the h-level hierarchy
  • Examples of proofs that only work at h-level 2 and why they fail