Changes
1 changed files (+1/-1)
-
-
@@ -558,7 +558,7 @@ theorem bind_join_equiv' [E : EndofunctorMonoid m] : joinFromBind (bindFromJoin-- 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 -- Unlike 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
-