More Curry-Howard stuff

Changes

1 changed files (+35/-17)

• Category.lean
  • @@ -2,27 +2,21 @@ import Mathlib
    /- Lean, the category! - Objects: Types - Morphisms: (Total) Functions + Objects: Types (propositions in logic) + Morphisms: Total functions (implication in logic) + + In Lean, all functions are total and always terminate. Resources: - https://raw.githubusercontent.com/BartoszMilewski/DaoFP/refs/heads/master/DaoFP.pdf - https://math.andrej.com/2016/08/06/hask-is-not-a-category/ - https://www.mit.edu/~xy/lean/ - https://tannerduve.github.io/files/monads.pdf + https://raw.githubusercontent.com/BartoszMilewski/DaoFP/refs/heads/master/DaoFP.pdf Great category theory book + https://math.andrej.com/2016/08/06/hask-is-not-a-category/ Hask is not a category + https://www.mit.edu/~xy/lean/ IAP 2026 Lean class + https://tannerduve.github.io/files/monads.pdf Monads in Lean + https://ncatlab.org/nlab/show/computational+trilogy#rosetta_stone Curry-Howard-Lambek correspondence TODO: Diagrams? -/ - -- Initial object - #check Empty - - -- Morphism from initial object - #check Empty.elim - - -- Terminal object - #check PUnit - -- Identity morphism #check id
  • @@ -32,11 +26,35 @@ TODO: Diagrams?
    -- Equality of morphisms #check funext - -- Sums (coproducts) + -- Initial object + #check False + -- Morphism from initial object + #check False.elim + -- Also isomorphic to initial object because Lean universes are not cumulative? + #check PEmpty + #check PEmpty.elim + -- Lean has universes to prevent Russell's paradox + + -- Terminal object + #check True + -- Morphism to terminal object + #check fun _ ↦ True.intro + -- Also isomorphic? + #check PUnit + + -- Sums (coproducts) (∧ in logic) #check Sum + -- Morphism from first type + #check Sum.inl + -- Morphism from second type + #check Sum.inl - -- Products + -- Products (∨ in logic) #check Prod + -- Morphism to first type + #check Prod.fst + -- Morphism to second type + #check Prod.snd -- Exponentials #check (· → ·)