Slides of a (very) informal lecture of mine on the Curry-Howard correspondence
1 inductive ℕ : Type 2 | zero : ℕ 3 | succ : ℕ → ℕ