Typos

Changes

1 changed files (+4/-3)

• Category.lean
  • @@ -284,12 +284,12 @@ instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) where
    /-- 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. + Note that this does not work for an arbitrary function between the hom-functor and `f` 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] - /-- Mapping and unmapping an element `m α` returns itself -/ + /-- Mapping and unmapping an element `f α` returns itself -/ theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] : yoneda (yoneda' y) = y := by simp [yoneda, yoneda']
  • @@ -307,11 +307,12 @@ instance [Cofunctor f] : Conatural (· → α) f (coyoneda' y) where
    theorem coyoneda_lemma (g : NaturalType (· → α) f) [Cofunctor f] [N : Conatural (· → α) f g] : coyoneda' (coyoneda g) x = g x := by simp [coyoneda, coyoneda', N.naturality] + /-- Same but for Coyoneda -/ theorem coyoneda_lemma' (y : f α) [Cofunctor f] : coyoneda (coyoneda' y) = y := by simp [coyoneda, coyoneda', Cofunctor.id_comap] - -- TODO: Applicatives + -- Applicative functors #check Applicative #check LawfulApplicative