{x x0 : PreCategory} {x1 : Functor x0 x} {x2 x3 : PreCategory} {x4 : Functor x3 x2} {x5 x6 : Functor x3 x0} {x7 : Functor x2 x} {x8 : NaturalTransformation (x7 o x4) (x1 o x6)} {x9 : Functor x2 x} {x10 : Functor x0 x0} {x11 : Functor x x} {x12 : @Isomorphic (_ -> _) x11 1%functor} {x13 : @Isomorphic (_ -> _) x10 1%functor} {x14 : @Isomorphic (_ -> _) x9 (x11 o x7)%functor} {x15 : @Isomorphic (_ -> _) x5 (x10 o x6)%functor} {x16 : @Isomorphic (_ -> _) x5 x6} {x17 : (x16 : Category.Core.morphism _ _ _) = (left_identity_natural_transformation_1 x6 o ((x13 : Category.Core.morphism _ _ _) oR x6 o (x15 : Category.Core.morphism _ _ _)))%natural_transformation} {x18 : @Isomorphic (_ -> _) x9 x7} {x19 : x18 ^-1 = (x14 ^-1 o (x12 ^-1 oR x7) o inverse (left_identity_natural_transformation_1 x7))%natural_transformation} : (x1 oL (x16 : Category.Core.morphism _ _ _) o (x1 oL x15 ^-1 o associator_1 x1 x10 x6 o (x1 oL x13 ^-1 o right_identity_natural_transformation_2 x1 o left_identity_natural_transformation_1 x1 o ((x12 : Category.Core.morphism _ _ _) oR x1) oR x6) o associator_2 x11 x1 x6 o (x11 oL x8) o associator_1 x11 x7 x4 o ((x14 : Category.Core.morphism _ _ _) oR x4)) o (x18 ^-1 oR x4))%natural_transformation = x8. Proof. t. Qed.
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.