Lemma ProductStrength1 : θ_Strength1 θ. Proof. intro X. apply nat_trans_eq_alt; intro x. eapply pathscomp0; [apply BinProductOfArrows_comp|]. apply pathsinv0, BinProduct_endo_is_identity. + rewrite BinProductOfArrowsPr1. eapply pathscomp0; [ | apply id_right]. apply maponpaths, (nat_trans_eq_pointwise (S11 X) x). + rewrite BinProductOfArrowsPr2. eapply pathscomp0; [ | apply id_right]. apply maponpaths, (nat_trans_eq_pointwise (S21 X) 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.