proposition: Lemma transport_cF_to_idtoiso s' d' u : @transport _ (fun m => morphism _ s' (Fm m d')) _ _ p u = components_of (Category.Morphisms.idtoiso (_ -> _) (ap Fm p) : morphism _ _ _) d' o u.
proof: Proof. case p; clear p; simpl; autorewrite with morphism; reflexivity. Qed.
imports: Category.Core Functor.Core FunctorCategory.Core NaturalTransformation.Core Category.Morphisms