Lemma Gθ_Strength2_int : θ_Strength2_int Gθ. Proof. intros F Ze Ze'. set (Z := pr1 Ze); set (Z' := pr1 Ze'). apply nat_trans_eq_alt; intro c; simpl. do 4 rewrite id_left. etrans. { apply pathsinv0, functor_comp. } apply pathsinv0; etrans. { apply pathsinv0, functor_comp. } apply maponpaths. generalize (nat_trans_eq_pointwise (θ_strength2 F Ze Ze') c); simpl. rewrite id_left. intro Hyp. apply pathsinv0, Hyp. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.PointedFunctorsComposition.