Daily Archives: 28 October 2013
The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible
Magic tricks are often entertaining, sometimes boring, and in some rarer cases astonishing. For me, the following trick belongs to the third type: the magician asks a volunteer in the audience to think of a natural number. The volunteer secretly … Continue reading
Posted in Code, Higher Inductive Types
45 Comments
Homotopy Type Theory 