Add more category theory TODOs

Changes

1 changed files (+2/-0)

• Category.lean
  • @@ -541,3 +541,5 @@ theorem bind_join_equiv [Monad m] [LawfulMonad m] : (bindFromJoin (m := m) (join
    theorem bind_join_equiv' [E : EndofunctorMonoid m] : joinFromBind (bindFromJoin E.join) x = E.join x := by simp + + -- TODO: Enrichment