Lemma bracket_Thm15_ok_part2 (Z: Ptd)(f : Ptd ⟦ Z, ptd_from_alg InitAlg ⟧): (theta H) ((alg_carrier _ InitAlg) ⊗ Z) · # H ⦃f⦄ · τ InitAlg = # (pr1 (ℓ (U Z))) (τ InitAlg) · ⦃f⦄. Proof. apply nat_trans_eq_alt. intro c. assert (h_eq := pr2 (pr1 (SpecializedGMIt_Thm15 Z f))). assert (h_eq' := maponpaths (fun m:EndC⟦_,pr1 InitAlg⟧ => (((aux_iso_1_inv Z):(_⟹_)) _)· m) h_eq); clear h_eq. *) assert (h_eq2' := maponpaths (fun m:EndC⟦_,pr1 InitAlg⟧ => (BinCoproductIn2 (CPEndC _ _))· m) h_eq'). clear h_eq'. assert (h_eq2'_inst := nat_trans_eq_pointwise h_eq2' c). clear h_eq2'. match goal with |[ H1 : _ = ?f |- _ = _ ] => intermediate_path f end. - clear h_eq2'_inst. apply BinCoproductIn2Commutes_right_in_ctx_dir. unfold aux_iso_1; simpl. rewrite id_right. rewrite id_left. do 3 rewrite <- assoc. apply BinCoproductIn2Commutes_right_in_ctx_dir. unfold nat_trans_id; simpl. rewrite id_left. apply BinCoproductIn2Commutes_right_in_ctx_dir. unfold nat_trans_fix_snd_arg_data. apply BinCoproductIn2Commutes_right_in_double_ctx_dir. rewrite <- assoc. apply maponpaths. eapply pathscomp0. 2: apply assoc. apply maponpaths. apply pathsinv0. apply BinCoproductIn2Commutes. - rewrite <- h_eq2'_inst. clear h_eq2'_inst. apply BinCoproductIn2Commutes_left_in_ctx_dir. repeat rewrite id_left. apply assoc. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. 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.whiskering. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation.