More resources yay

Changes

1 changed files (+5/-1)

• Category.lean
  • @@ -6,9 +6,10 @@ Objects: Types
    Morphisms: (Total) Functions Resources: - https://www.mit.edu/~xy/lean/ 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 -/ -- Initial object
  • @@ -549,3 +550,6 @@ theorem bind_join_equiv' [E : EndofunctorMonoid m] : joinFromBind (bindFromJoin
    -- TODO: Monad transformers -- TODO: Enrichment + + -- Unlike in Haskell, Lean is powerful enough that we can also use it for doing category theory in any category, not just the category Lean + #check CategoryTheory.Category