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 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· 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 · 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 · 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 · 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.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.