proposition: Lemma θ_Strength2_implies_θ_Strength2_int : θ_Strength2 → θ_Strength2_int.
proof: Proof. unfold θ_Strength2_int, θ_Strength2. intros T X Z Z'. assert (TXZZ'_inst := T X Z Z' (functor_compose (U Z) (functor_composite (U Z') X)) (lassociator_CAT (pr1 Z) (pr1 Z') X)). eapply pathscomp0. { apply TXZZ'_inst. } clear T TXZZ'_inst. apply nat_trans_eq_alt. intro c. cbn. rewrite id_left. rewrite <- assoc. apply maponpaths. etrans; [| apply id_right]. apply maponpaths. assert (functor_id_H := functor_id H (functor_compose (pr1 Z) (functor_composite (pr1 Z') X))). assert (functor_id_H_c := nat_trans_eq_pointwise functor_id_H c). etrans; [| apply functor_id_H_c]. clear functor_id_H functor_id_H_c. revert c. apply nat_trans_eq_pointwise. apply maponpaths. apply nat_trans_eq_alt. intro c; apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.Notation