Lemma bracket_Thm15_ok_part1 (Z: Ptd)(f : Ptd ⟦ Z, ptd_from_alg InitAlg ⟧): # U f = # (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. simpl in h_eq'. assert (h_eq1' := maponpaths (fun m:EndC⟦_,pr1 InitAlg⟧ => (BinCoproductIn1 (CPEndC _ _))· m) h_eq'); clear h_eq'. assert (h_eq1'_inst := nat_trans_eq_pointwise h_eq1' c); clear h_eq1'. match goal with |[ H1 : _ = ?f |- _ = _ ] => intermediate_path f end. - clear h_eq1'_inst. unfold coproduct_nat_trans_data; simpl. unfold coproduct_nat_trans_in1_data ; simpl. repeat rewrite <- assoc . apply BinCoproductIn1Commutes_right_in_ctx_dir. simpl. rewrite id_left. apply BinCoproductIn1Commutes_right_in_ctx_dir. simpl. rewrite id_left. apply BinCoproductIn1Commutes_right_in_ctx_dir. rewrite (@id_left EndC). rewrite id_left. apply BinCoproductIn1Commutes_right_in_ctx_dir. rewrite (@id_left EndC). apply BinCoproductIn1Commutes_right_dir. apply idpath. - rewrite <- h_eq1'_inst. clear h_eq1'_inst. apply BinCoproductIn1Commutes_left_in_ctx_dir. unfold nat_trans_id; simpl. rewrite id_left. repeat rewrite (id_left EndEndC). repeat rewrite (id_left EndC). unfold functor_fix_snd_arg_ob. repeat rewrite assoc. apply idpath. 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.