proposition: Theorem SigmaMonoidFromInitialAlgebra_is_initial : isInitial _ σ.
proof: Proof. intro asigma. induction asigma as [av [[aτ [[aμ aη] Hμη]] Hτ]]. red in Hτ. cbn in Hτ. set (It_inst := Iteration_I_H av aη aτ). set (h := pr11 It_inst). use tpair. - exists h. use tpair. 2: { exact tt. } assert (aux := pr21 It_inst). hnf in aux. split. + exact (pr1 aux). + red. split. 2: { red. exact (pr2 aux). } red. change (h ⊗^{ Mon_V} h · aμ = μ · h). destruct aux as [auxτ auxη]. fold h in auxτ, auxη. set (Mendler_inst := SpecialGenMendlerIterationWithActegoryAndStrength Mon_PtdV IV CV Act (t,,η) CP H HH I_{Mon_V} av θ aτ (ru^{Mon_V}_{t} · h) (initial_annihilates t) (left_whiskering_omega_cocont t) δ). intermediate_path (pr11 Mendler_inst). * apply path_to_ctr. red; split. -- change (t ⊗^{Mon_V}_{l} η · (h ⊗^{ Mon_V} h · aμ) = ru^{ Mon_V }_{ t} · h). etrans. 2: { apply monoidal_rightunitornat. } etrans. 2: { apply maponpaths. apply (pr12 Hμη). } repeat rewrite assoc. apply cancel_postcomposition. rewrite (bifunctor_equalwhiskers Mon_V). unfold functoronmorphisms2. rewrite assoc. etrans. { apply cancel_postcomposition. apply pathsinv0, (functor_comp (leftwhiskering_functor Mon_V t)). } rewrite auxη. apply pathsinv0, (bifunctor_equalwhiskers Mon_V). -- change (t ⊗^{Mon_V}_{l} τ · (h ⊗^{ Mon_V} h · aμ) = θ (t,, η) t · # H (h ⊗^{ Mon_V} h · aμ) · aτ). etrans. 2: { apply cancel_postcomposition. rewrite functor_comp. rewrite assoc. apply cancel_postcomposition. transparent assert (h_ptd : (PtdV⟦(t,,η),(av,,aη)⟧)). { exists h. exact auxη. } apply (lineator_is_nattrans_full Mon_PtdV Act Act H (lineator_linnatleft _ _ _ _ θ) (lineator_linnatright _ _ _ _ θ)_ _ _ _ h_ptd h). } etrans. 2: { repeat rewrite assoc'. apply maponpaths. rewrite assoc. apply pathsinv0, Hτ. } repeat rewrite assoc. apply cancel_postcomposition. change (t ⊗^{Mon_V}_{l} τ · h ⊗^{Mon_V} h = h ⊗^{Mon_V} #H h · av ⊗^{Mon_V}_{l} aτ). etrans. 2: { unfold functoronmorphisms1. rewrite assoc'. apply maponpaths. apply (functor_comp (leftwhiskering_functor Mon_V av)). } rewrite <- auxτ. etrans. { rewrite (bifunctor_equalwhiskers Mon_V). unfold functoronmorphisms2. rewrite assoc. apply cancel_postcomposition. apply pathsinv0, (functor_comp (leftwhiskering_functor Mon_V t)). } apply pathsinv0, (bifunctor_equalwhiskers Mon_V). * apply pathsinv0, path_to_ctr. red; split. -- change (t ⊗^{Mon_V}_{l} η · (μ · h) = ru^{ Mon_V }_{ t} · h). rewrite assoc. etrans. { apply cancel_postcomposition. apply (monoid_to_unit_right_law Mon_V (pr212 σ)). } apply idpath. -- change (t ⊗^{Mon_V}_{l} τ · (μ · h) = θ (t,, η) t · # H (μ · h) · aτ). rewrite assoc. etrans. { apply cancel_postcomposition. apply pathsinv0, (pr22 σ). } repeat rewrite assoc'. apply maponpaths. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, functor_comp. } rewrite assoc'. apply maponpaths. exact auxτ. - hnf. intros [ah Hyp]. use total2_paths_f. { apply (path_to_ctr _ _ It_inst). cbn in Hyp. split. + exact (pr11 Hyp). + exact (pr221 Hyp). } show_id_type. assert (aux: isaprop TYPE). { apply isapropdirprod. + apply isapropdirprod. * apply V. * apply isaprop_is_monoid_mor. + apply isapropunit. } apply aux. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.FunctorCoalgebras UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.Adamek UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.CompletelyIterativeAlgebras UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Actegories.CoproductsInActegories UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects UniMath.SubstitutionSystems.GeneralizedSubstitutionSystems UniMath.SubstitutionSystems.ActionScenarioForGenMendlerIteration_alt UniMath.SubstitutionSystems.SigmaMonoids