Oops forgot to prove category of endofunctors has identity morphisms

Changes

1 changed files (+6/-0)

• Category.lean
  • @@ -451,6 +451,8 @@ However, in some cases we can use monad transformers to compose them.
    /- "A monad is just a monoid in the category of endofunctors" + In fact, there is a bijection between the two! + https://old.reddit.com/r/math/comments/ap25mr/a_monad_is_a_monoid_in_the_category_of/ The category of Lean endofunctors
  • @@ -458,6 +460,10 @@ Objects: Endofunctors
    Morphisms: Natural transformations (we showed earlier that vertical composition produces another natural transformation) -/ + /-- Every object has an identity morphism -/ + instance [Functor f] [LawfulFunctor f] : Natural f f id := + ⟨by simp⟩ + /-- Vertical composition is associative -/ lemma nat_trans_comp_assoc (η : NaturalType f g) (μ : NaturalType g h) (ν : NaturalType h i) [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] [Functor h] [LawfulFunctor h] [Functor i] [LawfulFunctor i] : ((ν ∘ μ) ∘ η) x = (ν ∘ μ ∘ η) x := by