Lemma θ_Strength2_implies_θ_Strength2_int : θ_Strength2 → θ_Strength2_int. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation.