proposition: Lemma θ_Strength2_int_implies_θ_Strength2 : θ_Strength2_int → θ_Strength2.
proof: Proof. unfold θ_Strength2_int, θ_Strength2. intros T X Z Z' Y a. apply nat_trans_eq_alt. intro c. assert (TXZZ' := T X Z Z'). assert (TXZZ'c := nat_trans_eq_pointwise TXZZ' c). cbn in TXZZ'c. clear T TXZZ'. rewrite id_left in TXZZ'c. cbn. rewrite <- TXZZ'c; clear TXZZ'c. rewrite <- assoc. apply maponpaths. assert (functor_comp_H := functor_comp H (rassociator_CAT (pr1 Z) (pr1 Z') X) (a : functor_compose (U Z) (functor_composite (U Z') X) --> Y)). assert (functor_comp_H_c := nat_trans_eq_pointwise functor_comp_H c). cbn in functor_comp_H_c. etrans; [| apply functor_comp_H_c ]. clear functor_comp_H functor_comp_H_c. revert c. apply nat_trans_eq_pointwise. apply maponpaths. apply nat_trans_eq_alt. intro c; apply pathsinv0, id_left. 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