Truth about Types
summary
Claims that types, logic and category theory are interchangeable via the Curry-Howard-Lambek isomorphism and demonstrates concrete encodings: truth ↔ unit/terminal, falsehood ↔ void/initial, conjunction ↔ product, implication ↔ exponential. Uses Haskell examples and the simply typed lambda calculus as the programming model, shows how double negation ↔ CPS (continuation passing style) embeds classical logic, and invokes the Yoneda-style lemma to justify the CPS translation. Gives the actual categorical constructions (products, eval, uniqueness conditions) and shows they model proofs and program constructs.
AI-written summary · about
chapters (11)
- 0:00Start
- 16:36Proofs
- 31:16Initial Object in Set
- 36:40Terminal Object in Set
- 40:02Product (Elimination)
- 45:18Product (Universality)
- 50:46Function Object
- 54:34Currying
- 55:21Negation
- 58:17Cartesian Closed Category
- 59:23Curry-Howard-Lambek
related talks
55mKeynote: Propositions as Types
43mPropositions as Types
41mWar Time Proofs and Futuristic Programs
06mLightning Talk: Curry-Howard Correspondence
01h 15mA Crash Course in Category Theory
01h 52mIsomorphic Reasoning: Counting with Types Part 3
33mTheory & Models of Lambda Calculus: Typed and Untyped (Part 6)
38mPropositions as Types for Beginners in Haskell