Library UniMath.SubstitutionSystems.MultiSortedMonadConstruction_actegorical

this file is a follow-up of MultisortedMonadConstruction_alt, where the semantic signatures Signature are replaced by functors with tensorial strength and HSS by MHSS

based on the lax lineator constructed in Multisorted_actegories and transferred (through weak equivalence) to the strength notion of monoidal heterogeneous substitution systems (MHSS), a MHSS is constructed and a monad obtained through it

author: Ralph Matthes, 2023

notice: this file does not correspond to MultisortedMonadConstruction but to MultisortedMonadConstruction_alt, even though this is not indicated in the name

for the additions in 2023

for the instantiation to HSET

Require Import UniMath.Bicategories.PseudoFunctors.Examples.CurryingInBicatOfCats.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses.
Require Import UniMath.Bicategories.PseudoFunctors.Biadjunction.
Require Import UniMath.CategoryTheory.Categories.HSET.Univalence.

Local Open Scope cat.

Import BifunctorNotations.
Import MonoidalNotations.

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

Define the category of sorts

Let sort_cat : category := path_pregroupoid sort Hsort.

This represents "sort → C"

Let sortToC : category := SortIndexing.sortToC sort Hsort C.

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

Let BPsortToC : BinProducts sortToC := SortIndexing.BPsortToC sort Hsort _ BP.

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

Context (EsortToC2 : Exponentials BPsortToC2)

this requires exponentials in a higher space than before for MultiSortedSigToFunctor

(HC : Colims_of_shape nat_graph C).

Construction of a monad from a multisorted signature

Section monad.

  Local Definition sortToC2 := SortIndexing.sortToC2 sort Hsort C.
  Local Definition sortToC3 := SortIndexing.sortToC3 sort Hsort C.

  Let BCsortToC2 : BinCoproducts sortToC2 := SortIndexing.BCsortToC2 sort Hsort _ BC.

  Let IsortToC2 : Initial sortToC2 := SortIndexing.IsortToC2 sort Hsort _ IC.

  Local Definition HCsortToC : Colims_of_shape nat_graph sortToC := SortIndexing.CLsortToC sort Hsort C nat_graph HC.

  Local Definition HCsortToC2 : Colims_of_shape nat_graph sortToC2 := SortIndexing.CLsortToC2 sort Hsort C nat_graph HC.

  Local Definition MultiSortedSigToFunctor' : MultiSortedSig sort -> sortToC3 := MultiSortedSigToFunctor' sort Hsort C TC BP BC CC.

  Local Definition is_omega_cocont_MultiSortedSigToFunctor' : ∏ M : MultiSortedSig sort , is_omega_cocont (MultiSortedSigToFunctor' M)
    := is_omega_cocont_MultiSortedSigToFunctor' sort Hsort C TC BP BC eqsetPC CC EsortToC2 HC.

  Local Definition MultiSortedSigToStrength' : ∏ M : MultiSortedSig sort ,
        MultiSorted_actegorical.pointedstrengthfromselfaction_CAT sort Hsort C (MultiSortedSigToFunctor' M)
    := MultiSortedSigToStrength' sort Hsort C TC BP BC CC.

  Let Id_H : sortToC3 → sortToC3 := SubstitutionSystems.Id_H sortToC BCsortToC.

Construction of initial algebra for the omega-cocontinuous signature functor with lax lineator

  Definition DatatypeOfMultisortedBindingSig_CAT (sig : MultiSortedSig sort) :
    Initial (FunctorAlg (Id_H (MultiSortedSigToFunctor' sig))).
  Proof.
    use colimAlgInitial.
    - exact IsortToC2.
    - apply (LiftingInitial_alt.is_omega_cocont_Id_H _ _ _ (is_omega_cocont_MultiSortedSigToFunctor' sig)).
    - apply HCsortToC2.
  Defined.

the associated MHSS

  Definition MHSSOfMultiSortedSig_CAT (sig : MultiSortedSig sort) :
    mhss (monendocat_monoidal sortToC) (MultiSortedSigToFunctor' sig) (MultiSortedSigToStrength' sig).
  Proof.
    use (initial_alg_to_mhss (MultiSortedSigToStrength' sig) BCsortToC2).
    - apply BindingSigToMonad_actegorical.bincoprod_distributor_pointed_CAT.
    - exact IsortToC2.
    - apply HCsortToC2.
    - apply (is_omega_cocont_MultiSortedSigToFunctor' sig).
    - intro F. apply Initial_functor_precat.
    - intro F. apply (is_omega_cocont_pre_composition_functor F HCsortToC).
  Defined.

the associated initial Sigma-monoid

  Definition InitialSigmaMonoidOfMultiSortedSig_CAT (sig : MultiSortedSig sort) : Initial (SigmaMonoid (MultiSortedSigToStrength' sig)).
  Proof.
    use (SigmaMonoidFromInitialAlgebraInitial (MultiSortedSigToStrength' sig) BCsortToC2).
    - apply BindingSigToMonad_actegorical.bincoprod_distributor_pointed_CAT.
    - exact IsortToC2.
    - apply HCsortToC2.
    - apply (is_omega_cocont_MultiSortedSigToFunctor' sig).
    - intro F. apply Initial_functor_precat.
    - intro F. apply (is_omega_cocont_pre_composition_functor F HCsortToC).
  Defined.

the associated Sigma-monoid - defined separately

  Definition SigmaMonoidOfMultiSortedSig_CAT (sig : MultiSortedSig sort) : SigmaMonoid (MultiSortedSigToStrength' sig).
  Proof.
    apply mhss_to_sigma_monoid.
    exact (MHSSOfMultiSortedSig_CAT sig).
  Defined.

the associated monad

  Definition MonadOfMultiSortedSig_CAT (sig : MultiSortedSig sort) : Monad sortToC.
  Proof.
    use monoid_to_monad_CAT.
    use SigmaMonoid_to_monoid.
    - exact (MultiSortedSigToFunctor' sig).
    - exact (MultiSortedSigToStrength' sig).
    - exact (SigmaMonoidOfMultiSortedSig_CAT sig).
  Defined.

End monad.

End MBindingSig.

Section InstanceHSET.

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

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

  Let BPsortToSet : BinProducts sortToSet := SortIndexing.BPsortToSet sort Hsort.
  Let BPsortToSet2 : BinProducts sortToSet2 := SortIndexing.BPsortToSet2 sort Hsort.

  Definition EsortToSet2 : Exponentials BPsortToSet2.
  Proof.
    set (aux := category_binproduct sortToSet (path_pregroupoid sort Hsort)).
    set (BPaux' := BinProducts_functor_precat aux _ BinProductsHSET).
    assert (Hyp : Exponentials BPaux').
    { apply Exponentials_functor_HSET. }
    transparent assert (HypAdj : (equivalence_of_cats sortToSet2 [aux, SET ])).
    { apply currying_hom_equivalence. }
    use (exponentials_through_adj_equivalence_univalent_cats _ _ Hyp).
    2: { apply is_univalent_functor_category.
         apply is_univalent_HSET. }
    2: { do 2 apply is_univalent_functor_category.
         apply is_univalent_HSET. }
    transparent assert (HypAdj' : (adj_equivalence_of_cats (left_functor HypAdj))).
    { apply adjointification. }
    use tpair.
    2: { apply (adj_equivalence_of_cats_inv HypAdj'). }
  Defined.

  Definition MultiSortedSigToMonadHSET_viaCAT : MultiSortedSig sort → Monad (sortToSet).
  Proof.
    intros sig; simple refine (MonadOfMultiSortedSig_CAT sort Hsort HSET _ _ _ _ _ _ _ _ sig).
    - apply TerminalHSET.
    - apply InitialHSET.
    - apply BinProductsHSET.
    - apply BinCoproductsHSET.
    - intros; apply ProductsHSET.
    - apply CoproductsHSET.
    - change (Exponentials BPsortToSet2). apply EsortToSet2.
    - apply ColimsHSET_of_shape.
  Defined.

End InstanceHSET.