Theorem SigmaMonoidFromInitialAlgebra_is_initial : isInitial _ σ. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.FunctorCoalgebras. Require Import UniMath.CategoryTheory.coslicecat. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Adamek. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.CompletelyIterativeAlgebras. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Actegories.CoproductsInActegories. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Require Import UniMath.SubstitutionSystems.GeneralizedSubstitutionSystems. Require Import UniMath.SubstitutionSystems.ActionScenarioForGenMendlerIteration_alt. Require Import UniMath.SubstitutionSystems.SigmaMonoids. Import BifunctorNotations. Import MonoidalNotations. Theorem SigmaMonoidFromInitialAlgebra_is_initial : isInitial _ σ. Definition SigmaMonoidFromInitialAlgebraInitial : Initial (SigmaMonoid θ) := σ,,SigmaMonoidFromInitialAlgebra_is_initial.