x y (f : morphism C x y) : (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ F x y) (Category.Core.left_identity C x y f))) = @Build_Isomorphic (_ -> _) _ _ ((left_identity_natural_transformation_1 (p_morphism_of F f)) o ((p_identity_of F y oR p_morphism_of F f) o p_composition_of F x y y 1 f))%natural_transformation _. Proof. apply path_isomorphic; simpl. simpl rewrite (@p_left_identity_of_coherent _ C F x y f). path_natural_transformation. symmetry. etransitivity; apply Category.Core.left_identity. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Category.Morphisms FunctorCategory.Morphisms. Require Import Functor.Composition.Core. Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Require Import NaturalTransformation.Isomorphisms. Require Import NaturalTransformation.Paths. Require Import FunctorCategory.Core. Require Import Pseudofunctor.Core. Require Import HoTT.Tactics.