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