proposition: Lemma transport_quiver_dom (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 c' d: C) (p : c = c') (f : ArrC c d) : Fmap _ _ (Logic.transport (fun z => ArrC z d) p f) = Logic.transport (fun z => ArrD z (Fobj d)) (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