proposition: Lemma p_right_identity_of_coherent_iso_for_rewrite x y (f : morphism C x y) : (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ F x y) (Category.Core.right_identity C x y f))) = @Build_Isomorphic (_ -> _) _ _ ((right_identity_natural_transformation_1 (p_morphism_of F f)) o ((p_morphism_of F f oL p_identity_of F x) o p_composition_of F x x y f 1))%natural_transformation _.
proof: Proof. apply path_isomorphic; simpl. simpl rewrite (@p_right_identity_of_coherent _ C F x y f). path_natural_transformation. symmetry. etransitivity; apply Category.Core.left_identity. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Category.Morphisms FunctorCategory.Morphisms Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws NaturalTransformation.Isomorphisms NaturalTransformation.Paths FunctorCategory.Core Pseudofunctor.Core HoTT.Tactics