proposition: Lemma transport_quiver_cod (C D: Type) (ArrC : forall c c' : C, Type) (ArrD : forall d d' : D, Type) (Fobj : C -> D) (Fmap : forall c c' : C, (ArrC c c') -> (ArrD (Fobj c) (Fobj c'))) (c d d': C) (p : d = d') (f : ArrC c d) : Fmap _ _ (Logic.transport (fun z => ArrC c z) p f) = Logic.transport (fun z => ArrD (Fobj c) z) (f_equal (Fobj) p) (Fmap _ _ f).
proof: Proof. destruct p. reflexivity. 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