(This was originally posted to reddit, but since the response to it spawned this blog, I figured I’d repost it here. It could use some editing, but c’est la vie…)
So, I’ve wanted to write a post with a nice, simple but non-trivial logic result for a while now, but I’ve only now found a good reddit-friendly topic: In homotopy type theory, the negation of any type is a proposition.
Don’t let that cryptic sentence scare you! The point of the next ~8000 characters is to explain what that means, and why it’s true. First, a (very) rough sketch of type theory (skip below the line if you already know some type theory, or if you are optimistic.)
In type theory, we have terms and types. Terms inhabit types–to start, think of terms as “elements” and types as “sets”, but there are some crucial differences:
- A term…
View original post 1,348 more words