Oh yay the Yoneda proofs are less cursed now

Changes

1 changed files (+3/-4)

• Category.lean
  • @@ -112,6 +112,7 @@ A function type is covariant if the free param is in an even depth and contravar
    and so on -/ + /-- Composition of two functors of same variance is a functor -/ @[simp] instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] : Functor (f ∘ g) where
  • @@ -246,8 +247,7 @@ 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. -/ theorem yoneda_lemma (g : NaturalType (α → ·) f) [Functor f] [LawfulFunctor f] [N : Natural (α → ·) f g] : yoneda' (yoneda g) x = g x := by - unfold yoneda yoneda' - simp [N.naturality] + simp [yoneda, yoneda', N.naturality] /-- Mapping and unmapping an element `m α` returns itself -/ theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] : yoneda (yoneda' y) = y := by
  • @@ -266,8 +266,7 @@ instance [Cofunctor f] : Conatural (· → α) f (coyoneda' y) where
    /-- Same but for Coyoneda -/ theorem coyoneda_lemma (g : NaturalType (· → α) f) [Cofunctor f] [N : Conatural (· → α) f g] : coyoneda' (coyoneda g) x = g x := by - unfold coyoneda coyoneda' - simp [N.naturality] + simp [coyoneda, coyoneda', N.naturality] theorem coyoneda_lemma' (y : f α) [Cofunctor f] : coyoneda (coyoneda' y) = y := by simp [coyoneda, coyoneda', Cofunctor.id_comap]