Lemma Flat_θ_strength2_int: θ_Strength2_int Flat_θ. Proof. intros ? ? ?. apply nat_trans_eq_alt. intro c. cbn. repeat rewrite id_left. rewrite id_right. repeat rewrite <- functor_comp. apply maponpaths. repeat rewrite functor_id. rewrite id_right. set (c' := pr1 X (pr1 Z' (pr1 Z c))). change (pr1 (ptd_pt C Z) c' · pr1 (ptd_pt C Z') (pr1 (pr1 (pr1 Z)) c') = pr1 (pr2 Z') c' · # (pr1 Z') (pr1 (pr2 Z) c')). etrans. 2: { apply (nat_trans_ax (pr2 Z')). } apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. 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.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.BinSumOfSignatures. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.