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