I’ve started studying homotopy type theory in earnest. What started six months ago as an expedition into Haskell and type systems now takes me deeper and deeper into the underlying mathematics. The reasons aren’t strictly because I believe this to be of benefit to my programming. It is more because I’ve grown fond of structures, algebras, categories, and more as I delve in typed functional programming. Math strikes me as really interesting, and I didn’t realize this until I started exploring functional programming and inductive reasoning.
For the time being, I’ve duplicated a nifty table from the Homotopy Type Theory Book below. It summarizes the equivalences between types, logic, sets, ands homotopy, much in the spirit of the Curry-Howard-Lambek isomorphism or its intuitionistic logic counterpart the Brouwer-Heyting-Kolomogriv correspondence.
Enjoy!
| Types | Logic | Sets | Homotopy |
|---|---|---|---|
| A | proposition | set | space |
| a : A | proof | element | point |
| B(x) | predicate | family of sets | fibration |
| b(x) : B(x) | conditional proof | family of elements | section |
| 0,1 | ⊥ , ⊤ | ∅, {∅} | ∅, * |
| A + B | A ∨ B | disjoint union | coproduct |
| A × B | A ∧ B | set of pairs | product space |
| A → B | A ⇒ B | set of functions | function space |
| Σ(x : A)B(x) | ∃x : AB(x) | disjoint sum | total space |
| Π(x : A)B(x) | ∀x : AB(x) | product | space of sections |
| IdA | equality= | {(x, x)|x ∈ A} | path space AI |