Warming up to Homotopy Type Theory

pigworker in a space

“Why do you hate homotopy type theory?” is question I am sometimes asked, but I never answer it, because the question has an inaccurate presupposition. I am not happy when people forget that function extensionality, a key benefit of HoTT, was already available in Observational Type Theory. I am not happy when people disregard the convenience of having a clearly delimited fragment of one’s propositions where proofs can be identified definitionally. I am not happy when people act as if homotopy type theory already works when, without an internal notion of computation which gives canonical forms (like OTT has), it doesn’t…yet. But I’m pretty sure it will acquire such a notion. So, for the avoidance of doubt, I do not hate homotopy type theory: I hate homotopy type theorists almost as much as I hate myself, which is why I have decided to become a homotopy type theorist as…

View original post 2,179 more words

This entry was posted in Philosophie. Bookmark the permalink.