(s d : object) (m : morphism s d) : compose (identity _) m = m. Proof. refine (@path_morphism' _ _ (compose (identity _) m) m (Category.Core. _ _ _ _) (Category.Core. _ _ _ _) _). simpl in *. repeat match goal with | [ |- context[@morphism_inverse _ _ _ _ (@isisomorphism_isomorphic _ _ _ (Category.Morphisms.idtoiso ?C0 (ap (p_morphism_of ?F (s:=_) (d:=_)) (Category.Core. ?C ?x ?y ?f))))] ] => generalize (@p_left_identity_of_coherent_inverse_for_rewrite _ C F x y f); generalize (Category.Morphisms.idtoiso C0 (ap (p_morphism_of F (s:=_) (d:=_)) (Category.Core. C x y f))) | [ |- context[Category.Morphisms.idtoiso ?C0 (ap (p_morphism_of ?F (s:=_) (d:=_)) (Category.Core. ?C ?x ?y ?f))] ] => generalize (@p_left_identity_of_coherent_for_rewrite _ C F x y f); generalize (Category.Morphisms.idtoiso C0 (ap (p_morphism_of F (s:=_) (d:=_)) (Category.Core. C x y f))) end. simpl. destruct_head morphism. destruct_head object. simpl in *. repeat match goal with | [ |- context[p_composition_of ?F ?x ?y ?z ?m1 ?m2] ] => generalize dependent (p_composition_of F x y z m1 m2) | [ |- context[p_identity_of ?F ?x] ] => generalize dependent (p_identity_of F x) | [ |- context[p_morphism_of ?F ?x] ] => generalize dependent (p_morphism_of F x) | [ |- context[p_object_of ?F ?x] ] => generalize dependent (p_object_of F x) end. simpl. clear. repeat (let H := fresh "x" in intro H). repeat match goal with H : _ |- _ => revert H end. intro. >> *)
Require Import Functor.Core NaturalTransformation.Core. Require Import Category.Strict. Require Import Functor.Composition.Core. Require Import NaturalTransformation.Paths NaturalTransformation.Composition.Core. Require Import Category.Morphisms FunctorCategory.Core. Require Import Pseudofunctor.Core Pseudofunctor.RewriteLaws. Require Import NaturalTransformation.Composition.Laws. Require Import FunctorCategory.Morphisms. Require Import HoTT.Tactics. Import Functor.Identity.FunctorIdentityNotations. Module Import LaxCommaCategory.