Remove unnecessary type class params

Changes

1 changed files (+3/-2)

• Category.lean
  • @@ -76,6 +76,7 @@ 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) + /-- This is not standard notation but I just made something up -/ infixr:100 " <¥> " => Cofunctor.comap theorem Cofunctor.id_comap' [Cofunctor f] : Cofunctor.comap (f := f) (@id α) = id := by
  • @@ -328,7 +329,7 @@ theorem coyoneda_lemma' (y : f α) [Cofunctor f] : coyoneda (coyoneda' y) = y :=
    /-- Composition of two applicatives is an applicative -/ @[simp] - instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicative g] : Applicative (f ∘ g) where + instance [Applicative f] [Applicative g] : Applicative (f ∘ g) where pure x := pure (f := f) (pure x) seq h x := Seq.seq (f := f) ((· <*> ·) <$> h) x
  • @@ -453,7 +454,7 @@ https://old.reddit.com/r/math/comments/ap25mr/a_monad_is_a_monoid_in_the_categor
    The category of Lean endofunctors Objects: Endofunctors - Morphisms: Natural transformations + Morphisms: Natural transformations (we showed earlier that vertical composition produces another natural transformation) -/ /-- Vertical composition is associative -/