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. 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 H HH Z _ Ghat rhohat (thetahat Z f)). intermediate_path (pr1 (pr1 X)). - set (TT := @fusion_law EndC InitialEndC Colims_of_shape_nat_graph_EndC Id_H (is_omega_cocont_Id_H H HH) _ (pr1 (InitAlg)) T'). set (Psi := ψ_from_comps (Id_H) _ (ℓ (U Z)) (Const_plus_H C CP H (U Z)) (ρ_Thm15 H HH Z f) (aux_iso_1 H Z · θ'_Thm15 H Z (nat_trans_fix_snd_arg _ _ _ _ _ θ Z) · aux_iso_2_inv H Z) ). set (T2 := TT _ (HU Z) (isInitial_pre_comp Z) Psi). set (T3 := T2 (ℓ (U Z)) (HU Z)). set (Psi' := ψ_from_comps (Id_H) _ (ℓ (U Z)) (Ghat) (rhohat) (iso1' Z · thetahat_0 Z f · iso2' Z) ). set (T4 := T3 (isInitial_pre_comp Z) Psi'). set (Φ := (Phi_fusion Z T' β)). set (T5 := T4 Φ). intermediate_path (Φ _ (fbracket InitHSS Z f)); try apply idpath. etrans; [| apply T5 ]; clear TT T2 T3 T4 T5 X. * now apply cancel_postcomposition. * apply funextsec; intro t. apply nat_trans_eq_alt; intro c; simpl. rewrite !id_right. apply BinCoproductArrow_eq_cor. + rewrite <- !assoc. apply BinCoproductIn1Commutes_left_in_ctx_dir, BinCoproductIn1Commutes_right_in_ctx_dir. simpl; rewrite id_left. apply BinCoproductIn1Commutes_left_in_ctx_dir, 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, BinCoproductIn1Commutes_right_in_ctx_dir. simpl; rewrite id_left. now apply BinCoproductIn1Commutes_right_dir. + rewrite <- !assoc. apply BinCoproductIn2Commutes_left_in_ctx_dir, BinCoproductIn2Commutes_right_in_ctx_dir. simpl; rewrite id_left. apply BinCoproductIn2Commutes_left_in_ctx_dir, BinCoproductIn2Commutes_right_in_ctx_dir. simpl; rewrite <- !assoc. apply maponpaths, BinCoproductIn2Commutes_left_in_ctx_dir, BinCoproductIn2Commutes_right_in_ctx_dir. simpl. rewrite <- !assoc. etrans; [| eapply pathsinv0, cancel_postcomposition, (nat_trans_eq_pointwise (functor_comp H t β) c) ]. simpl; rewrite <- assoc. apply maponpaths, BinCoproductIn2Commutes_left_in_ctx_dir. assert (Hyp_c := nat_trans_eq_pointwise (τ_part_of_alg_mor _ CP _ _ _ (InitialArrow IA (pr1 T'))) c). simpl in Hyp_c. etrans; [ eapply pathsinv0, Hyp_c |]. now apply maponpaths, pathsinv0, BinCoproductIn2Commutes. - apply pathsinv0, path_to_ctr. apply nat_trans_eq_alt; intro c. simpl; rewrite id_right. apply BinCoproductArrow_eq_cor. + rewrite <- !assoc. apply BinCoproductIn1Commutes_right_in_ctx_dir. simpl; rewrite id_left. apply BinCoproductIn1Commutes_right_in_ctx_dir. simpl; rewrite <- assoc. etrans; [| apply maponpaths, BinCoproductIn1Commutes_right_in_ctx_dir; simpl; rewrite id_left; apply BinCoproductIn1Commutes_right_dir, idpath ]. rewrite !assoc. assert (fbracket_η_inst_c := nat_trans_eq_pointwise (fbracket_η T' (f · #U(ptd_from_alg_mor _ CP H β0))) c). etrans; [| apply (!fbracket_η_inst_c) ]. apply cancel_postcomposition, (ptd_mor_commutes _ (ptd_from_alg_mor _ CP H β0) ((pr1 Z) 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 β))· θ ((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. 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.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.All. 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_alt. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation.