More style tweaks

Changes

1 changed files (+6/-3)

• Category.lean
  • @@ -281,8 +281,11 @@ def yoneda' [Functor f] [LawfulFunctor f] (y : f α) : NaturalType (α → ·) f
    instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) where naturality h x := by simp [yoneda']; rfl - /-- Mapping and unmapping a natural transformation returns the itself - Note that this does work for an arbitrary function between the hom-functor and `m` because we use the naturality condition. -/ + /-- + Mapping and unmapping a natural transformation returns the itself + + Note that this does work for an arbitrary function between the hom-functor and `m` because we use the naturality condition. + -/ theorem yoneda_lemma (g : NaturalType (α → ·) f) [Functor f] [LawfulFunctor f] [N : Natural (α → ·) f g] : yoneda' (yoneda g) x = g x := by simp [yoneda, yoneda', N.naturality]
  • @@ -290,7 +293,6 @@ theorem yoneda_lemma (g : NaturalType (α → ·) f) [Functor f] [LawfulFunctor
    theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] : yoneda (yoneda' y) = y := by simp [yoneda, yoneda'] - /-- Coyoneda forward map -/ def coyoneda (g : NaturalType (· → α) f) [Cofunctor f] : f α := g id
  • @@ -331,6 +333,7 @@ instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicativ
    ext simp [seq_assoc] + -- TODO: Monads #check Monad #check LawfulMonad