(F G : Functor B C) (T U : NaturalTransformation F G) (a : A) (b : B) (f : H a <~=~> b) (H' : T oR H = U oR H) : T b = U b. Proof. apply (ap components_of) in H'. apply apD10 in H'; hnf in H'; simpl in H'. rewrite <- !(path_components_of_isomorphic' f). rewrite H'. reflexivity. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Functorial.Core. Require Import NaturalTransformation.Composition.Core. Require Import NaturalTransformation.Isomorphisms. Require Import Functor.Attributes. Require Import FunctorCategory.Core. Require Import Category.Morphisms. Require Import NaturalTransformation.Paths. Require Import HoTT.Truncations.Core.