x1 x2 x3 x4 (m1 : morphism x1 x2) (m2 : morphism x2 x3) (m3 : morphism x3 x4) : compose (compose m3 m2) m1 = compose m3 (compose m2 m1). Proof. refine (@path_morphism' _ A B S T _ _ (compose (compose m3 m2) m1) (compose m3 (compose m2 m1)) (Category.Core. _ _ _ _ _ _ _ _) (Category.Core. _ _ _ _ _ _ _ _) _). simpl. apply associativity_helper. - exact (p_composition_of_coherent_for_rewrite _ _ _ _ _ _ _ _). - exact (p_composition_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.