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. apply iso_moveR_pV. symmetry. apply commutes. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import NaturalTransformation.Composition.Core. Require Import Functor.Composition.Core. Require Import Category.Morphisms. Require Import FunctorCategory.Core. Require Import NaturalTransformation.Paths. Require Import Basics.Tactics.