Better notation I guess

Changes

1 changed files (+7/-5)

• Category.lean
  • @@ -75,13 +75,15 @@ class Cofunctor (f : Type u → Type v) where
    id_comap (x : f α) : comap id x = x comp_comap (g : β → α) (h : γ → β) (x : f α) : comap (g ∘ h) x = comap h (comap g x) + infixr:100 " <¥> " => Cofunctor.comap + theorem Cofunctor.id_comap' [Cofunctor f] : Cofunctor.comap (f := f) (@id α) = id := by ext x exact Cofunctor.id_comap (f := f) x theorem Cofunctor.comap_comp_comap [Cofunctor f] (g : α → β) (h : β → γ) : - ((Cofunctor.comap g) ∘ (Cofunctor.comap h) : f γ → f α) = Cofunctor.comap (f := f) (h ∘ g) := - funext fun _ => (comp_comap _ _ _).symm + ((g <¥> ·) ∘ (h <¥> ·) : f γ → f α) = Cofunctor.comap (f := f) (h ∘ g) := + funext fun _ ↦ (comp_comap _ _ _).symm /-- Hom-functor in enriched category -/
  • @@ -138,7 +140,7 @@ instance [Cofunctor f] [Cofunctor g] : LawfulFunctor (f ∘ g) where
    /-- Composition of functors of opposite variance is a contravariant functor -/ @[simp] instance [Functor f] [LawfulFunctor f] [Cofunctor g] : Cofunctor (f ∘ g) where - comap h x := Functor.map (f := f) (Cofunctor.comap h ·) x + comap h x := Functor.map (f := f) (h <¥> ·) x id_comap := by simp [Cofunctor.id_comap (f := g)] comp_comap := by simp [Cofunctor.comp_comap]
  • @@ -231,7 +233,7 @@ instance : Natural Option List OptionToList where
    grind class Conatural f [Cofunctor f] g [Cofunctor g] (η : NaturalType f g) where - naturality (h : β → α) (x : f α) : Cofunctor.comap h (η x) = η (Cofunctor.comap h x) + naturality (h : β → α) (x : f α) : h <¥> (η x) = η (h <¥> x) /-- Yoneda forward map (g is not necessarily natural) -/
  • @@ -258,7 +260,7 @@ theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] : yoneda (yoneda'
    def coyoneda (g : NaturalType (· → α) f) [Cofunctor f] : f α := g id /-- Coyoneda reverse map -/ - def coyoneda' [Cofunctor f] (y : f α) : NaturalType (· → α) f := (Cofunctor.comap · y) + def coyoneda' [Cofunctor f] (y : f α) : NaturalType (· → α) f := (· <¥> y) /-- Reverse map always produces a natural transformation -/ instance [Cofunctor f] : Conatural (· → α) f (coyoneda' y) where