proposition: Lemma transport_functorial_dom (C D: Category) (F : @Functor C D) (c c' d : C) (p : c = c') (f : hom c d) : fmap[F] (transport (fun z => hom z d) p f) = transport (fun z => hom z (fobj[F] d)) (f_equal (fobj[F]) p) (fmap[F] f).
proof: Proof. destruct p. reflexivity. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Equations.Prop.Logic