Library UniMath.SubstitutionSystems.SimplifiedHSS.MonadicSubstitution_alt

Shows global results that do not fit into a particular file but rather put the different strands together. We focus on the results that are based on omega-cocontinuity (and not the existence of right Kan extensions), which also explains the suffix "_alt" to the proper file name.

Written by Ralph Matthes, 2021

version for simplified notion of HSS by Ralph Matthes (2022, 2023) the file is identical to the homonymous file in the parent directory, except for importing files from the present directory

Set Kernel Term Sharing.

Require Import UniMath.Foundations.PartD.

Require Import UniMath.MoreFoundations.PartA.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Monads.Monads.
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.PointedFunctors.
Require Import UniMath.SubstitutionSystems.Signatures.
Require Import UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems.
Require Import UniMath.SubstitutionSystems.SimplifiedHSS.MonadsFromSubstitutionSystems.
Require Import UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt.
Require Import UniMath.SubstitutionSystems.Notation.
Local Open Scope subsys.

Local Open Scope cat.

Section MainResult.

Context (C : category) (CP : BinCoproducts C).
Context (IC : Initial C) (CC : Colims_of_shape nat_graph C).

Local Notation "'EndC'":= ([C , C ]) .
Local Notation "'Ptd'" := (category_Ptd C).

Let CPEndC : BinCoproducts EndC := BinCoproducts_functor_precat _ _ CP.
Let EndEndC := [EndC , EndC ].
Let CPEndEndC:= BinCoproducts_functor_precat _ _ CPEndC: BinCoproducts EndEndC.

Let InitialEndC : Initial EndC.
Proof.
apply Initial_functor_precat, IC.
Defined.

Let Colims_of_shape_nat_graph_EndC : Colims_of_shape nat_graph EndC.
Proof.
apply ColimsFunctorCategory_of_shape, CC.
Defined.

Context (H : functor [C , C ] [C , C ])
        (θ : StrengthForSignature H)
        (HH : is_omega_cocont H).

Let Const_plus_H (X : EndC) : functor EndC EndC := Const_plus_H C CP H X.

Let Id_H : functor [C , C ] [C , C ] := Id_H C CP H.

Definition TermHSS : hss_category CP (Presignature_Signature (H ,,θ)) :=
  InitHSS C CP IC CC (Presignature_Signature (H ,,θ)) HH.

Definition TermHetSubst: heterogeneous_substitution C CP H
  := hetsubst_from_hss C CP (Presignature_Signature (H ,,θ)) TermHSS.

Definition Terms: [C , C ] := pr1 (pr1 TermHSS).
Definition TermAlgebra: FunctorAlg Id_H:= pr1 TermHSS.

Goal TermAlgebra = InitAlg C CP IC CC H HH.
Proof.
  apply idpath.
Qed.

Definition isInitialTermAlgebra: isInitial (FunctorAlg Id_H) TermAlgebra.
Proof.
  set (aux := colimAlgInitial InitialEndC (is_omega_cocont_Id_H C CP H HH) (Colims_of_shape_nat_graph_EndC _)).
  exact (pr2 aux).
Defined.

Definition TermMonad: Monad C := Monad_from_hss C CP (H ,,θ) TermHSS.

Definition VarTerms: [C , C ] ⟦ functor_identity C , Terms ⟧:= eta_from_alg TermAlgebra.

Definition ConstrTerms: [C , C ] ⟦ H Terms , Terms ⟧ := tau_from_alg TermAlgebra.

Goal ConstrTerms = τ TermHetSubst.
Proof.
  apply idpath.
Qed.

Definition join: [C , C ] ⟦ functor_compose Terms Terms , Terms ⟧ := prejoin_from_hetsubst TermHetSubst.

Goal join = μ TermMonad.
Proof.
  apply idpath.
Qed.

Definition joinLookup:
  ∏ c : C , pr1 VarTerms (pr1 Terms c) · pr1 join c = identity (pr1 Terms c)
  := @Monad_law1 C TermMonad.

Definition θforTerms := θ_from_hetsubst C CP H TermHetSubst Terms.

Goal θforTerms = PrecategoryBinProduct.nat_trans_fix_snd_arg_data [C , C ] Ptd [C , C ]
         (θ_source H ) (θ_target H ) (pr1 θ ) (ptd_from_alg (InitAlg C CP IC CC H HH )) Terms.
Proof.
  apply idpath.
Qed.

Definition joinHomomorphic: θforTerms · # H join · ConstrTerms =
                  #(pre_composition_functor _ _ _ Terms ) ConstrTerms · join
  := prejoin_from_hetsubst_τ TermHetSubst.

Definition joinHasEtaLaw:
  ∏ c : C , # (pr1 Terms ) (pr1 VarTerms c ) · pr1 join c = identity (pr1 Terms c)
  := @Monad_law2 C TermMonad.

Definition joinHasPermutationLaw:
  ∏ c : C , # (pr1 Terms ) (pr1 join c ) · pr1 join c = pr1 join (pr1 Terms c) · pr1 join c
  := @Monad_law3 C TermMonad.

End MainResult.