proposition: Lemma path_components_of_isisomorphism' `{IsIsomorphism C s d m} D (F G : Functor C D) (T : NaturalTransformation F G) : (G _1 m o T s) o (F _1 m)^-1 = T d.
proof: Proof. apply iso_moveR_pV. symmetry. apply commutes. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Composition.Core Functor.Composition.Core Category.Morphisms FunctorCategory.Core NaturalTransformation.Paths Basics.Tactics