Monthly Archives: February 2014
Composition is not what you think it is! Why “nearly invertible” isn’t.
A few months ago, Nicolai Kraus posted an interesting and surprising result: the truncation map 
: ℕ → ‖ℕ‖ is nearly invertible. This post attempts to explain why “nearly invertible” is a misnomer. I, like many others, was very … Continue reading
The surreals contain the plump ordinals
The very last section of the book presents a constructive definition of Conway’s surreal numbers as a higher inductive-inductive type. Conway’s classical surreals include the ordinal numbers; so it’s natural to wonder whether, or in what sense, this may be … Continue reading
Another proof that univalence implies function extensionality
The fact, due to Voevodsky, that univalence implies function extensionality, has always been a bit mysterious to me—the proofs that I have seen have all seemed a bit non-obvious, and I have trouble re-inventing or explaining them. Moreover, there are … Continue reading
Homotopy Type Theory 