{x x0 : PreCategory} {x1 : Functor x0 x} {x2 x3 : PreCategory} {x4 : Functor x3 x2} {x5 x6 : PreCategory} {x7 : Functor x6 x5} {x8 x9 : PreCategory} {x10 : Functor x9 x8} {x11 : Functor x9 x6} {x12 : Functor x9 x3} {x13 : Functor x0 x6} {x14 : Functor x9 x6} {x15 : Functor x8 x5} {x16 : Functor x x5} {x17 : Functor x9 x0} {x18 : Functor x8 x} {x19 : NaturalTransformation (x18 o x10) (x1 o x17)} {x20 : Functor x0 x3} {x21 : Functor x x2} {x22 : NaturalTransformation (x21 o x1) (x4 o x20)} {x23 : Functor x8 x2} {x24 : Functor x3 x6} {x25 : Functor x2 x5} {x26 : NaturalTransformation (x25 o x4) (x7 o x24)} {x27 : Functor x8 x5} {x28 : @Isomorphic (_ -> _) x27 (x25 o x23)%functor} {x29 : @Isomorphic (_ -> _) x23 (x21 o x18)%functor} {x30 : @Isomorphic (_ -> _) x16 (x25 o x21)%functor} {x31 : @Isomorphic (_ -> _) x15 (x16 o x18)%functor} {x32 : @Isomorphic (_ -> _) x14 (x13 o x17)%functor} {x33 : @Isomorphic (_ -> _) x13 (x24 o x20)%functor} {x34 : @Isomorphic (_ -> _) x12 (x20 o x17)%functor} {x35 : @Isomorphic (_ -> _) x11 (x24 o x12)%functor} {x36 : @Isomorphic (_ -> _) x14 x11} (x37 : (x36 : Category.Core.morphism _ _ _) = (x35 ^-1 o (x24 oL x34 ^-1 o (associator_1 x24 x20 x17 o ((x33 : Category.Core.morphism _ _ _) oR x17 o (x32 : Category.Core.morphism _ _ _)))))%natural_transformation) {x38 : @Isomorphic (_ -> _) x15 x27} (x39 : x38 ^-1 = (x31 ^-1 o (x30 ^-1 oR x18) o inverse (associator_1 x25 x21 x18) o (x25 oL (x29 : Category.Core.morphism _ _ _)) o (x28 : Category.Core.morphism _ _ _))%natural_transformation) : (x7 oL (x36 : Category.Core.morphism _ _ _) o (x7 oL x32 ^-1 o associator_1 x7 x13 x17 o (x7 oL x33 ^-1 o associator_1 x7 x24 x20 o (x26 oR x20) o associator_2 x25 x4 x20 o (x25 oL x22) o associator_1 x25 x21 x1 o ((x30 : Category.Core.morphism _ _ _) oR x1) oR x17) o associator_2 x16 x1 x17 o (x16 oL x19) o associator_1 x16 x18 x10 o ((x31 : Category.Core.morphism _ _ _) oR x10)) o (x38 ^-1 oR x10))%natural_transformation = (x7 oL x35 ^-1 o associator_1 x7 x24 x12 o (x26 oR x12) o associator_2 x25 x4 x12 o (x25 oL (x4 oL x34 ^-1 o associator_1 x4 x20 x17 o (x22 oR x17) o associator_2 x21 x1 x17 o (x21 oL x19) o associator_1 x21 x18 x10 o ((x29 : Category.Core.morphism _ _ _) oR x10))) o associator_1 x25 x23 x10 o ((x28 : Category.Core.morphism _ _ _) oR x10))%natural_transformation. 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.