Lemma θ_Strength2_int_implies_θ_Strength2 : θ_Strength2_int → θ_Strength2. 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.
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.