proposition: Lemma associativity_helper {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: Proof. t. Qed.
imports: Functor.Core NaturalTransformation.Core Category.Strict Functor.Composition.Core NaturalTransformation.Paths NaturalTransformation.Composition.Core Category.Morphisms FunctorCategory.Core Pseudofunctor.Core Pseudofunctor.RewriteLaws NaturalTransformation.Composition.Laws FunctorCategory.Morphisms HoTT.Tactics