More examples of category theory in Lean

Changes

1 changed files (+2/-0)

• Category.lean
  • @@ -553,3 +553,5 @@ theorem bind_join_equiv' [E : EndofunctorMonoid m] : joinFromBind (bindFromJoin
    -- 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 + #check CategoryTheory.Functor + #check CategoryTheory.yoneda