Nope. Okay, thanks for coming. But seriously, this question is genuinely interesting. Since we as humans understand what we want when we talk about numbers such as 0 or 1, and understand that such notions are distinct, then our theory of natural numbers should also reflect that difference. That is to say, we know that …
In this blog post, we will be following the very excellent paper [1]. Anyone looking for a good introduction that focuses less on the formal proofs should definitely give it a read! Let us consider the most important object in the study of homotopy theory, the unit interval, The way we analytically understand this object …
Cubical Type Theory: The Unit Interval and Paths Read More »