proposition: Proposition transport_r_comp (C : Category) (c c' d e : C) (p : c = c') (f : hom c' d) (g : hom d e) : Logic.transport_r (fun z => hom z e) p (g ∘ f) = g ∘ (Logic.transport_r (fun z => hom z d) p f).
proof: Proof. now destruct p. Defined.
imports: Category.Lib Category.Lib.TList Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Adjunction Category.Theory.Universal.Arrow Category.Instance.StrictCat Category.Construction.Groupoid Category.Construction.Opposite Category.Construction.Product Category.Instance.Sets