Lemma ProductStrength2 : θ_Strength2 θ. Proof. intros X Z Z' Y α. apply nat_trans_eq_alt; intro x. eapply pathscomp0; [ apply BinProductOfArrows_comp |]. apply pathsinv0. eapply pathscomp0; [ apply cancel_postcomposition; simpl; apply BinProductOfArrows_comp|]. eapply pathscomp0; [ apply BinProductOfArrows_comp|]. apply pathsinv0, maponpaths_12. - assert (Ha := S12 X Z Z' Y α); simpl in Ha. apply (nat_trans_eq_pointwise Ha x). - assert (Ha := S22 X Z Z' Y α); simpl in Ha. apply (nat_trans_eq_pointwise Ha x). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. 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.BinProducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.exponentials.