Homotopy, Sets, Logic, and Types

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.


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