proposition: Lemma isfaithful_precomposition_essentially_surjective_helper (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: 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.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Functorial.Core NaturalTransformation.Composition.Core NaturalTransformation.Isomorphisms Functor.Attributes FunctorCategory.Core Category.Morphisms NaturalTransformation.Paths HoTT.Truncations.Core