Library UniMath.SubstitutionSystems.SimplifiedHSS.MultiSortedMonadConstruction_alt

This file contains the final steps of the formalization of multisorted binding signatures:
Written by: Anders Mörtberg, 2021. The formalization is an adaptation of Multisorted.v
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
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Products.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.Exponentials.
Require Import UniMath.CategoryTheory.Chains.All.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.CategoryTheory.Categories.HSET.Core.
Require Import UniMath.CategoryTheory.Categories.HSET.Colimits.
Require Import UniMath.CategoryTheory.Categories.HSET.Limits.
Require Import UniMath.CategoryTheory.Categories.HSET.Structures.
Require Import UniMath.CategoryTheory.Categories.StandardCategories.
Require Import UniMath.CategoryTheory.Groupoids.

Require Import UniMath.SubstitutionSystems.Signatures.
Require Import UniMath.SubstitutionSystems.SumOfSignatures.
Require Import UniMath.SubstitutionSystems.BinProductOfSignatures.
Require Import UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems.
Require Import UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt.
Require Import UniMath.SubstitutionSystems.SimplifiedHSS.MonadsFromSubstitutionSystems.
Require Import UniMath.SubstitutionSystems.SignatureExamples.
Require UniMath.SubstitutionSystems.SortIndexing.
Require Import UniMath.SubstitutionSystems.SimplifiedHSS.BindingSigToMonad.
Require Import UniMath.SubstitutionSystems.MultiSortedBindingSig.
Require Import UniMath.SubstitutionSystems.MultiSorted_alt.

Local Open Scope cat.

Section MBindingSig.

Context (sort : UU) (Hsort : isofhlevel 3 sort) (C : category).

Context (TC : Terminal C) (IC : Initial C)
        (BP : BinProducts C) (BC : BinCoproducts C)
         (eqsetPC : forall (s s' : sort), Products (s=s') C)
        (CC : forall (I : UU), isaset I → Coproducts I C).

Local Notation "'1'" := (TerminalObject TC).
Local Notation "a ⊕ b" := (BinCoproductObject (BC a b)).

This represents "sort → C"
Let sortToC : category := SortIndexing.sortToC sort Hsort C.

Let BCsortToC : BinCoproducts sortToC := SortIndexing.BCsortToC sort Hsort _ BC.

Let BPsortToCC : BinProducts [sortToC,C] := SortIndexing.BPsortToCC sort Hsort _ BP.

Context (EsortToCC : Exponentials BPsortToCC)
        (HC : Colims_of_shape nat_graph C).

Construction of a monad from a multisorted signature

Section monad.

Let Id_H := Id_H sortToC BCsortToC.

Definition SignatureInitialAlgebra
  (H : Signature sortToC sortToC sortToC) (Hs : is_omega_cocont H) :
  Initial (FunctorAlg (Id_H H)).
Show proof.
use colimAlgInitial.
- apply Initial_functor_precat, Initial_functor_precat, IC.
- apply (is_omega_cocont_Id_H), Hs.
- apply ColimsFunctorCategory_of_shape, ColimsFunctorCategory_of_shape, HC.

Let HSS := @hss_category _ BCsortToC.

Definition MultiSortedSigToHSS (sig : MultiSortedSig sort) :
  HSS (MultiSortedSigToSignature sort Hsort C TC BP BC CC sig).
Show proof.
apply SignatureToHSS.
+ apply Initial_functor_precat, IC.
+ apply ColimsFunctorCategory_of_shape, HC.
+ apply is_omega_cocont_MultiSortedSigToSignature.
  - exact eqsetPC.
  - exact EsortToCC.
  - exact HC.

Definition MultiSortedSigToHSSisInitial (sig : MultiSortedSig sort) :
  isInitial _ (MultiSortedSigToHSS sig).
Show proof.
now unfold MultiSortedSigToHSS, SignatureToHSS; destruct InitialHSS.

Function from multisorted binding signatures to monads

Definition MultiSortedSigToMonad (sig : MultiSortedSig sort) : Monad sortToC.
Show proof.
use Monad_from_hss.
- apply BCsortToC.
- apply (MultiSortedSigToSignature sort Hsort C TC BP BC CC sig).
- apply MultiSortedSigToHSS.

End monad.

End MBindingSig.

Section MBindingSigMonadHSET.

Context (sort : UU) (Hsort : isofhlevel 3 sort).

Let sortToSet : category := SortIndexing.sortToSet sort Hsort.

Definition projSortToSet : sort → functor sortToSet HSET :=
  projSortToC sort Hsort HSET.

Definition hat_functorSet : sort → HSET ⟶ sortToSet :=
  hat_functor sort Hsort HSET CoproductsHSET.

Definition sorted_option_functorSet : sort → sortToSet ⟶ sortToSet :=
  sorted_option_functor _ Hsort HSET
                        TerminalHSET BinCoproductsHSET CoproductsHSET.

Definition MultiSortedSigToSignatureSet : MultiSortedSig sort → Signature sortToSet sortToSet sortToSet.
Show proof.
use MultiSortedSigToSignature.
- apply TerminalHSET.
- apply BinProductsHSET.
- apply BinCoproductsHSET.
- apply CoproductsHSET.

Definition MultiSortedSigToMonadSet (ms : MultiSortedSig sort) :
  Monad sortToSet.
Show proof.
use MultiSortedSigToMonad.
- apply TerminalHSET.
- apply InitialHSET.
- apply BinProductsHSET.
- apply BinCoproductsHSET.
- intros. apply ProductsHSET.
- apply CoproductsHSET.
- apply Exponentials_functor_HSET.
- apply ColimsHSET_of_shape.
- apply ms.

End MBindingSigMonadHSET.