(s d : object) (m : morphism s d) : compose (identity _) m = m. Proof. refine (@path_morphism' _ A B S T _ _ (compose (identity _) m) m (Category.Core. _ _ _ _) (Category.Core. _ _ _ _) _). simpl. refine left_identity_helper. - exact (p_left_identity_of_coherent_for_rewrite _ _ _ _). - exact (p_left_identity_of_coherent_inverse_for_rewrite _ _ _ _). Defined.
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.