Lemma ishssMor_InitAlg (T' : hss CP H) : @ishssMor C CP H InitHSS T' (InitialArrow IA (pr1 T') : @algebra_mor EndC Id_H InitAlg T' ). Proof. unfold ishssMor. unfold isbracketMor. intros Z f. set (β0 := InitialArrow IA (pr1 T')). match goal with | [|- _ · ?b = _ ] => set (β := b) end. set ( rhohat := BinCoproductArrow (CPEndC _ _ ) β (tau_from_alg T') : pr1 Ghat T' --> T'). set (X:= SpecializedGMIt Z _ Ghat rhohat (thetahat Z f)). intermediate_path (pr1 (pr1 X)). - set (TT:= fusion_law _ _ IA _ (pr1 InitAlg) T' _ (KanExt Z)). set (Psi := ψ_from_comps _ (Id_H) _ _ (ℓ (U Z)) (Const_plus_H (U Z)) (ρ_Thm15 Z f) (aux_iso_1 Z · θ'_Thm15 Z · aux_iso_2_inv Z) ). set (T2 := TT Psi). set (T3 := T2 (ℓ (U Z)) (KanExt Z)). set (Psi' := ψ_from_comps _ (Id_H) _ _ (ℓ (U Z)) (Ghat) (rhohat) (iso1' Z · thetahat_0 Z f · iso2' Z) ). set (T4 := T3 Psi'). set (Φ := (Phi_fusion Z T' β)). set (T5 := T4 Φ). intermediate_path (Φ _ (fbracket InitHSS Z f)). + apply idpath. + eapply pathscomp0. 2: { apply T5. apply funextsec. intro t. simpl. unfold compose. simpl. apply nat_trans_eq_alt. simpl. intro c. rewrite id_right. rewrite id_right. apply BinCoproductArrow_eq_cor. * clear TT T2 T3 T4 T5. do 5 rewrite <- assoc. apply BinCoproductIn1Commutes_left_in_ctx_dir. apply BinCoproductIn1Commutes_right_in_ctx_dir. simpl. rewrite id_left. apply BinCoproductIn1Commutes_left_in_ctx_dir. apply BinCoproductIn1Commutes_right_in_ctx_dir. simpl. rewrite id_left. apply BinCoproductIn1Commutes_left_in_ctx_dir. simpl. rewrite id_left. apply BinCoproductIn1Commutes_left_in_ctx_dir. rewrite <- assoc. apply maponpaths. apply BinCoproductIn1Commutes_right_in_ctx_dir. simpl. rewrite id_left. apply BinCoproductIn1Commutes_right_dir. apply idpath. * clear TT T2 T3 T4 T5. do 5 rewrite <- assoc. apply BinCoproductIn2Commutes_left_in_ctx_dir. apply BinCoproductIn2Commutes_right_in_ctx_dir. rewrite (@id_left EndC). apply BinCoproductIn2Commutes_left_in_ctx_dir. apply BinCoproductIn2Commutes_right_in_ctx_dir. simpl. unfold nat_trans_fix_snd_arg_data. repeat rewrite <- assoc. apply maponpaths. apply BinCoproductIn2Commutes_left_in_ctx_dir. apply BinCoproductIn2Commutes_right_in_ctx_dir. simpl. assert (H_nat_inst := functor_comp H t β). assert (H_nat_inst_c := nat_trans_eq_pointwise H_nat_inst c); clear H_nat_inst. { match goal with |[ H1 : _ = ?f |- _ = _· ?g · ?h ] => intermediate_path (f·g·h) end. + clear H_nat_inst_c. simpl. repeat rewrite <- assoc. apply maponpaths. apply BinCoproductIn2Commutes_left_in_ctx_dir. simpl. unfold coproduct_nat_trans_in2_data, coproduct_nat_trans_data. assert (Hyp := τ_part_of_alg_mor _ CP _ _ _ (InitialArrow IA (pr1 T'))). assert (Hyp_c := nat_trans_eq_pointwise Hyp c); clear Hyp. simpl in Hyp_c. etrans; [ eapply pathsinv0; exact Hyp_c |]. clear Hyp_c. apply maponpaths. apply pathsinv0. apply BinCoproductIn2Commutes. + rewrite <- H_nat_inst_c. apply idpath. } } apply cancel_postcomposition. apply idpath. - apply pathsinv0. apply path_to_ctr. apply nat_trans_eq_alt. intro c. simpl. rewrite id_right. apply BinCoproductArrow_eq_cor. + repeat rewrite <- assoc. apply BinCoproductIn1Commutes_right_in_ctx_dir. simpl. unfold coproduct_nat_trans_in1_data, coproduct_nat_trans_in2_data, coproduct_nat_trans_data. rewrite id_left. apply BinCoproductIn1Commutes_right_in_ctx_dir. simpl. repeat rewrite <- assoc. etrans. 2: { apply maponpaths. apply BinCoproductIn1Commutes_right_in_ctx_dir. rewrite id_left. apply BinCoproductIn1Commutes_right_dir. apply idpath. } do 2 rewrite assoc. etrans. { apply cancel_postcomposition. assert (ptd_mor_commutes_inst := ptd_mor_commutes _ (ptd_from_alg_mor _ CP H β0) ((pr1 Z) c)). apply ptd_mor_commutes_inst. } assert (fbracket_η_inst := fbracket_η T' (f · #U (ptd_from_alg_mor _ CP H β0))). assert (fbracket_η_inst_c := nat_trans_eq_pointwise fbracket_η_inst c); clear fbracket_η_inst. apply (!fbracket_η_inst_c). + repeat rewrite <- assoc. apply BinCoproductIn2Commutes_right_in_ctx_dir. simpl. unfold coproduct_nat_trans_in1_data, coproduct_nat_trans_in2_data, coproduct_nat_trans_data. rewrite id_left. apply BinCoproductIn2Commutes_right_in_ctx_dir. unfold nat_trans_fix_snd_arg_data. simpl. unfold coproduct_nat_trans_in2_data. repeat rewrite <- assoc. etrans. 2: { apply maponpaths. apply BinCoproductIn2Commutes_right_in_ctx_dir. rewrite <- assoc. apply maponpaths. apply BinCoproductIn2Commutes_right_dir. apply idpath. } do 2 rewrite assoc. etrans. { apply cancel_postcomposition. eapply pathsinv0. assert (τ_part_of_alg_mor_inst := τ_part_of_alg_mor _ CP H _ _ β0). assert (τ_part_of_alg_mor_inst_Zc := nat_trans_eq_pointwise τ_part_of_alg_mor_inst ((pr1 Z) c)); clear τ_part_of_alg_mor_inst. apply τ_part_of_alg_mor_inst_Zc. } simpl. unfold coproduct_nat_trans_in2_data. repeat rewrite <- assoc. etrans. { apply maponpaths. rewrite assoc. eapply pathsinv0. assert (fbracket_τ_inst := fbracket_τ T' (f · #U (ptd_from_alg_mor _ CP H β0))). assert (fbracket_τ_inst_c := nat_trans_eq_pointwise fbracket_τ_inst c); clear fbracket_τ_inst. apply fbracket_τ_inst_c. } simpl. unfold coproduct_nat_trans_in2_data. repeat rewrite assoc. apply cancel_postcomposition. apply cancel_postcomposition. assert (Hyp: ((# (pr1 (ℓ(U Z))) (# H β))· (theta H) ((alg_carrier _ T') ⊗ Z)· # H (fbracket T' _ (f · #U(ptd_from_alg_mor C CP H β0))) = θ (tpair (λ _ : functor C C, ptd_obj C) (alg_carrier _ (InitialObject IA)) Z) · # H (# (pr1 (ℓ(U Z))) β · fbracket T' _ (f · #U(ptd_from_alg_mor C CP H β0))))). 2: { assert (Hyp_c := nat_trans_eq_pointwise Hyp c); clear Hyp. exact Hyp_c. } clear c. clear X. clear rhohat. rewrite (functor_comp H). rewrite assoc. apply cancel_postcomposition. fold θ. apply nat_trans_eq_alt. intro c. assert (θ_nat_1_pointwise_inst := θ_nat_1_pointwise _ _ _ H θ _ _ β Z c). etrans ; [exact θ_nat_1_pointwise_inst | ]. clear θ_nat_1_pointwise_inst. simpl. apply maponpaths. rewrite horcomp_id_prewhisker. 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.SimplifiedHSS.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.