Add more newlines

Changes

1 changed files (+5/-0)

• Category.lean
  • @@ -326,6 +326,7 @@ theorem coyoneda_lemma' (y : f α) [Cofunctor f] : coyoneda (coyoneda' y) = y :=
    -- Motivation: mapping multi-arg functions #simp (some 3).map (· * ·) + #eval (· * ·) <$> (some 3) <*> (some 4) /-- Composition of two applicatives is an applicative -/
  • @@ -559,7 +560,11 @@ 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 + #check CategoryTheory.Monad + #check CategoryTheory.Monad.monadMonEquiv