/longform/

series

the mathematical holy trinity

There is a set of three equivalences between category theory (algebra), type theory (computation), and logic (proofs) that are known as the Curry-Howard-Lambek correspondence. I find these relationships fascinating and want to explore them further. Not only in a theoretical way, but also in a practical way for designing safe and scalable software. Ultimately, I want to get into programming languages that offer theorem proving and venture deep into homotopy type theory and higher categories.

algebra as computation

It's good to start with an example, and one I am quite fond of is the construction with vector spaces by creating sum types and product types. These all are miraculously ubiquitous objects whether you are in physics, computer science, or mathematics. We will see how one can go from the algebraic perspective straight into implementation and how we can extract additional features of these objects naturally.

2024-04-17