Library UniMath.SubstitutionSystems.MultiSorted_alt

This file contains a formalization of multisorted binding signatures:
Written by: Anders Mörtberg, 2021. The formalization is an adaptation of Multisorted.v
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.Combinatorics.Lists.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
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.Adjunctions.Core.
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.SubstitutionSystems.
Require Import UniMath.SubstitutionSystems.LiftingInitial_alt.
Require Import UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems.
Require Import UniMath.SubstitutionSystems.SignatureExamples.
Require Import UniMath.SubstitutionSystems.BindingSigToMonad.

Local Open Scope cat.

Arguments Gθ_Signature {_ _ _ _} _ _.
Arguments Signature_Functor {_ _ _} _.
Arguments BinProduct_of_functors {_ _} _ _ _.
Arguments DL_comp {_ _} _ {_} _.
Arguments θ_from_δ_Signature {_ _} _.
Arguments BinProduct_of_Signatures {_ _ _} _ _ _.
Arguments Sum_of_Signatures _ {_ _ _} _ _.

Definition of multisorted binding signatures

Section MBindingSig.

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

Variables (TC : Terminal C) (IC : Initial C)
          (BP : BinProducts C) (BC : BinCoproducts C)
          (PC : ∀ (I : UU), Products I C) (CC : ∀ (I : UU), isaset I → Coproducts I C).

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

Define the discrete category of sorts
Let sort_cat : category := path_pregroupoid sort Hsort.

This represents "sort → C"
Let sortToC : category := [sort_cat,C].
Let make_sortToC (f : sort → C) : sortToC := functor_path_pregroupoid Hsort f.

Let BCsortToC : BinCoproducts sortToC := BinCoproducts_functor_precat _ _ BC.
Let BPC : BinProducts [sortToC,C] := BinProducts_functor_precat sortToC C BP.

Variables (expSortToCC : Exponentials BPC)
          (HC : Colims_of_shape nat_graph C).

Definition of multisorted signatures
Definition MultiSortedSig : UU :=
  ∑ (I : hSet), I → list (list sort × sort) × sort.

Definition ops (M : MultiSortedSig) : hSet := pr1 M.
Definition arity (M : MultiSortedSig) : ops M → list (list sort × sort) × sort :=
  λ x, pr2 M x.

Definition mkMultiSortedSig {I : hSet}
  (ar : I → list (list sort × sort) × sort) : MultiSortedSig := (I,,ar).

Sum of multisorted binding signatures
Definition SumMultiSortedSig : MultiSortedSig → MultiSortedSig → MultiSortedSig.
Proof.
intros s1 s2.
use tpair.
- apply (setcoprod (ops s1) (ops s2)).
- induction 1 as [i|i].
  + apply (arity s1 i).
  + apply (arity s2 i).
Defined.

Construction of an endofunctor on C^sort,C^sort from a multisorted signature

Section functor.

Given a sort s this applies the sortToC to s and returns C
Definition projSortToC (s : sort) : functor sortToC C.
Proof.
use tpair.
+ use tpair.
  - intro f; apply (pr1 f s).
  - simpl; intros a b f; apply (f s).
+ abstract (split; intros f *; apply idpath).
Defined.

Definition hat_functor (t : sort) : functor C sortToC.
Proof.
use tpair.
+ use tpair.
  - intros A.
    use make_sortToC; intros s.
    use (CoproductObject (t = s) C (CC _ (Hsort t s) (λ _, A))).
  - intros a b f.
    apply (nat_trans_functor_path_pregroupoid); intros s.
    apply CoproductOfArrows; intros p; apply f.
+ split.
  - abstract (intros x; apply nat_trans_eq_alt; intros s;
    apply pathsinv0, CoproductArrowUnique; intros p;
    now rewrite id_left, id_right).
  - abstract (intros x y z f g; apply nat_trans_eq_alt; intros s;
    apply pathsinv0, CoproductArrowUnique; intros p; cbn;
    now rewrite assoc, (CoproductOfArrowsIn _ _ (CC _ (Hsort t s) (λ _, x))),
            <- !assoc, (CoproductOfArrowsIn _ _ (CC _ (Hsort t s) (λ _, y)))).
Defined.

Section Sorted_Option_Functor.

Context (s : sort).

Definition option_fun_summand : sortToC.
Proof.
apply make_sortToC; intro t.
exact (CoproductObject (t = s) C (CC _ (Hsort t s) (λ _, 1))).
Defined.

Definition sorted_option_functor : functor sortToC sortToC :=
  constcoprod_functor1 BCsortToC option_fun_summand.

the following two definitions are currently not used

Local Definition Some_sorted_option_functor : functor_identity sortToC ⟹ sorted_option_functor :=
  BinCoproductIn2 (BinCoproducts_functor_precat _ _ BCsortToC
                                                  (constant_functor _ _ option_fun_summand)
                                                  (functor_identity sortToC)).

Local Definition None_sorted_option_functor : constant_functor _ _ option_fun_summand ⟹ sorted_option_functor :=
  BinCoproductIn1 (BinCoproducts_functor_precat _ _ BCsortToC
                                                  (constant_functor _ _ option_fun_summand)
                                                  (functor_identity sortToC)).

End Sorted_Option_Functor.

Sorted option functor for lists
Definition option_list (xs : list sort) : [sortToC,sortToC].
Proof.
use (foldr1 (λ F G, F ∙ G) (functor_identity _) (map sorted_option_functor xs)).
Defined.

Define a functor
F^(l,t)(X) := projSortToC(t) ∘ X ∘ sorted_option_functor(l)
if l is nonempty and
F^(l,t)(X) := projSortToC(t) ∘ X
otherwise
Definition exp_functor (lt : list sort × sort) : functor [sortToC,sortToC] [sortToC,C].
Proof.
induction lt as [l t].
use (list_ind _ _ _ l); clear l.
- exact (post_comp_functor (projSortToC t)).
- intros s l _.
  exact (pre_comp_functor (option_list (cons s l)) ∙ post_comp_functor (projSortToC t)).
Defined.

This defines F^lts where lts is a list of (l,t). Outputs a product of functors if the list is nonempty and otherwise the constant functor.
Definition exp_functor_list (xs : list (list sort × sort)) :
  functor [sortToC,sortToC] [sortToC,C].
Proof.
set (T := constant_functor [sortToC,sortToC] [sortToC,C]
                           (constant_functor sortToC C TC)).
set (XS := map exp_functor xs).
exact (foldr1 (λ F G, BinProduct_of_functors BPC F G) T XS).
Defined.

Definition hat_exp_functor_list (xst : list (list sort × sort) × sort) :
  functor [sortToC,sortToC] [sortToC,sortToC] :=
    exp_functor_list (pr1 xst) ∙ post_comp_functor (hat_functor (pr2 xst)).

The function from multisorted signatures to functors
Definition MultiSortedSigToFunctor (M : MultiSortedSig) :
  functor [sortToC,sortToC] [sortToC,sortToC].
Proof.
use (coproduct_of_functors (ops M)).
+ apply Coproducts_functor_precat, Coproducts_functor_precat, CC, setproperty.
+ intros op.
  exact (hat_exp_functor_list (arity M op)).
Defined.

End functor.

Construction of the strength for the endofunctor on C^sort,C^sort

derived from a multisorted signature
Section strength.

Definition DL_sorted_option_functor (s : sort) :
  DistributiveLaw sortToC (sorted_option_functor s) :=
    genoption_DistributiveLaw sortToC (option_fun_summand s) BCsortToC.

Definition DL_option_list (xs : list sort) : DistributiveLaw _ (option_list xs).
Proof.
induction xs as [[|n] xs].
+ induction xs.
  apply DL_id.
+ induction n as [|n IH].
  × induction xs as [m []].
    apply DL_sorted_option_functor.
  × induction xs as [m [k xs]].
    apply (DL_comp (DL_sorted_option_functor m) (IH (k,,xs))).
Defined.

Definition Sig_exp_functor (lt : list sort × sort) :
  Signature sortToC C sortToC.
Proof.
∃ (exp_functor lt).
induction lt as [l t]; revert l.
use list_ind.
+ exact (pr2 (Gθ_Signature (IdSignature _ _) (projSortToC t))).
+ intros x xs H; simpl.
  set (Sig_option_list := θ_from_δ_Signature (DL_option_list (cons x xs))).
  apply (pr2 (Gθ_Signature Sig_option_list (projSortToC t))).
Defined.

Local Lemma functor_in_Sig_exp_functor_ok (lt : list sort × sort) :
  Signature_Functor (Sig_exp_functor lt) = exp_functor lt.
Proof.
apply idpath.
Qed.

Definition Sig_exp_functor_list (xs : list (list sort × sort)) :
  Signature sortToC C sortToC.
Proof.
∃ (exp_functor_list xs).
induction xs as [[|n] xs].
- induction xs.
  exact (pr2 (ConstConstSignature _ _ _ _)).
- induction n as [|n IH].
  + induction xs as [m []].
    exact (pr2 (Sig_exp_functor m)).
  + induction xs as [m [k xs]].
    exact (pr2 (BinProduct_of_Signatures _ (Sig_exp_functor _) (tpair _ _ (IH (k,,xs))))).
Defined.

Local Lemma functor_in_Sig_exp_functor_list_ok (xs : list (list sort × sort)) :
  Signature_Functor (Sig_exp_functor_list xs) = exp_functor_list xs.
Proof.
apply idpath.
Qed.

Definition Sig_hat_exp_functor_list (xst : list (list sort × sort) × sort) :
  Signature sortToC sortToC sortToC.
Proof.
apply (Gθ_Signature (Sig_exp_functor_list (pr1 xst)) (hat_functor (pr2 xst))).
Defined.

Local Lemma functor_in_Sig_hat_exp_functor_list_ok (xst : list (list sort × sort) × sort) :
  Signature_Functor (Sig_hat_exp_functor_list xst) = hat_exp_functor_list xst.
Proof.
apply idpath.
Qed.

Definition MultiSortedSigToSignature (M : MultiSortedSig) : Signature sortToC sortToC sortToC.
Proof.
set (Hyps := λ (op : ops M), Sig_hat_exp_functor_list (arity M op)).
use (Sum_of_Signatures (ops M) _ Hyps).
apply Coproducts_functor_precat, CC, setproperty.
Defined.

Local Lemma functor_in_MultiSortedSigToSignature_ok (M : MultiSortedSig) :
  Signature_Functor (MultiSortedSigToSignature M) = MultiSortedSigToFunctor M.
Proof.
apply idpath.
Qed.

End strength.

Proof that the functor obtained from a multisorted signature is omega-cocontinuous

Section omega_cocont.

Local Definition projSortToC_rad (t : sort) : functor C sortToC.
Proof.
use tpair.
+ use tpair.
  - intros A.
    use make_sortToC; intros s.
    exact (ProductObject (t = s) C (PC _ (λ _, A))).
  - intros a b f.
    apply (nat_trans_functor_path_pregroupoid); intros s.
    apply ProductOfArrows; intros p; apply f.
+ split.
  - abstract (intros x; apply nat_trans_eq_alt; intros s;
    apply pathsinv0, ProductArrowUnique; intros p;
    now rewrite id_left, id_right).
  - abstract(intros x y z f g; apply nat_trans_eq_alt; intros s; cbn;
    now rewrite ProductOfArrows_comp).
Defined.

Local Lemma is_left_adjoint_projSortToC (s : sort) : is_left_adjoint (projSortToC s).
Proof.
∃ (projSortToC_rad s).
use make_are_adjoints.
- use make_nat_trans.
  + intros A.
    use make_nat_trans.
    × intros t; apply ProductArrow; intros p; induction p; apply identity.
    × abstract (now intros a b []; rewrite id_right, (functor_id A), id_left).
  + abstract (intros A B F; apply nat_trans_eq_alt; intros t; cbn;
    rewrite precompWithProductArrow, postcompWithProductArrow;
    apply ProductArrowUnique; intros []; cbn;
    now rewrite (ProductPrCommutes _ _ _ (PC _ (λ _, pr1 B s))), id_left, id_right).
- use make_nat_trans.
  + intros A.
    exact (ProductPr _ _ (PC _ (λ _, A)) (idpath _)).
  + abstract (now intros a b f; cbn; rewrite (ProductOfArrowsPr _ _ (PC _ (λ _, b)))).
- use make_form_adjunction.
  + intros A; cbn.
    now rewrite (ProductPrCommutes _ _ _ (PC _ (λ _, pr1 A s))).
  + intros c; apply nat_trans_eq_alt; intros t; cbn.
    rewrite postcompWithProductArrow.
    apply pathsinv0, ProductArrowUnique; intros [].
    now rewrite !id_left.
Qed.

Local Lemma is_omega_cocont_post_comp_projSortToC (s : sort) :
  is_omega_cocont (post_comp_functor (A := sortToC) (projSortToC s)).
Proof.
apply is_omega_cocont_post_composition_functor.
apply is_left_adjoint_projSortToC.
Defined.

Local Lemma is_omega_cocont_exp_functor (a : list sort × sort) :
  is_omega_cocont (exp_functor a).
Proof.
induction a as [xs t]; revert xs.
use list_ind.
- apply is_omega_cocont_post_comp_projSortToC.
- intros x xs H; simpl.
  apply is_omega_cocont_functor_composite.
  + apply (is_omega_cocont_pre_composition_functor (option_list _)).
    apply (ColimsFunctorCategory_of_shape nat_graph sort_cat _ HC).
  + apply is_omega_cocont_post_comp_projSortToC.
Defined.

Local Lemma is_omega_cocont_exp_functor_list (xs : list (list sort × sort)) :
  is_omega_cocont (exp_functor_list xs).
Proof.
induction xs as [[|n] xs].
- induction xs.
  apply is_omega_cocont_constant_functor.
- induction n as [|n IHn].
  + induction xs as [m []].
    apply is_omega_cocont_exp_functor.
  + induction xs as [m [k xs]].
    apply is_omega_cocont_BinProduct_of_functors.
    × apply BinProducts_functor_precat, BinProducts_functor_precat, BP.
    × apply is_omega_cocont_constprod_functor1.
      apply expSortToCC.
    × apply is_omega_cocont_exp_functor.
    × apply (IHn (k,,xs)).
Defined.

Local Lemma is_left_adjoint_hat (s : sort) : is_left_adjoint (hat_functor s).
Proof.
∃ (projSortToC s).
use make_are_adjoints.
- use make_nat_trans.
  + intros A.
    exact (CoproductIn _ _ (CC (s = s) _ (λ _, A)) (idpath _)).
  + abstract (now intros A B f; cbn; rewrite (CoproductOfArrowsIn _ _ (CC _ _ (λ _, A)))).
- use make_nat_trans.
  + intros A.
    use make_nat_trans.
    × intros t; apply CoproductArrow; intros p.
      exact (transportf (λ z, C ⟦ pr1 A s , z ⟧) (maponpaths (pr1 A) p) (identity _)).
    × abstract (intros a b []; now rewrite id_left, (functor_id A), id_right).
  + abstract (intros A B F;
    apply nat_trans_eq_alt; intros t; cbn;
    rewrite precompWithCoproductArrow, postcompWithCoproductArrow;
    apply CoproductArrowUnique; intros []; cbn;
    now rewrite id_left, (CoproductInCommutes _ _ _ (CC _ _ (λ _, pr1 A s))), id_right).
- use make_form_adjunction.
  + intros c; apply nat_trans_eq_alt; intros t; cbn.
    rewrite precompWithCoproductArrow.
    apply pathsinv0, CoproductArrowUnique; intros [].
    now rewrite !id_right.
  + intros A; cbn.
    now rewrite (CoproductInCommutes _ _ _ (CC _ _ (λ _, pr1 A s))).
Qed.

Local Lemma is_omega_cocont_post_comp_hat_functor (s : sort) :
  is_omega_cocont (post_comp_functor (A := sortToC) (hat_functor s)).
Proof.
apply is_omega_cocont_post_composition_functor, is_left_adjoint_hat.
Defined.

Local Lemma is_omega_cocont_hat_exp_functor_list (xst : list (list sort × sort) × sort) :
  is_omega_cocont (hat_exp_functor_list xst).
Proof.
  apply is_omega_cocont_functor_composite.
  + apply is_omega_cocont_exp_functor_list.
  + apply is_omega_cocont_post_comp_hat_functor.
Defined.

The functor obtained from a multisorted binding signature is omega-cocontinuous
Lemma is_omega_cocont_MultiSortedSigToFunctor (M : MultiSortedSig) :
  is_omega_cocont (MultiSortedSigToFunctor M).
Proof.
  apply is_omega_cocont_coproduct_of_functors.
  intros op; apply is_omega_cocont_hat_exp_functor_list.
Defined.

Lemma is_omega_cocont_MultiSortedSigToSignature (M : MultiSortedSig) :
  is_omega_cocont (MultiSortedSigToSignature M).
Proof.
  apply is_omega_cocont_MultiSortedSigToFunctor.
Defined.

End omega_cocont.

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

Let HSS := @hss_category _ BCsortToC.

Definition MultiSortedSigToHSS (sig : MultiSortedSig) :
  HSS (MultiSortedSigToSignature sig).
Proof.
apply SignatureToHSS.
+ apply Initial_functor_precat, IC.
+ apply ColimsFunctorCategory_of_shape, HC.
+ apply is_omega_cocont_MultiSortedSigToSignature.
Defined.

Definition MultiSortedSigToHSSisInitial (sig : MultiSortedSig) :
  isInitial _ (MultiSortedSigToHSS sig).
Proof.
now unfold MultiSortedSigToHSS, SignatureToHSS; destruct InitialHSS.
Qed.

Function from multisorted binding signatures to monads

Definition MultiSortedSigToMonad (sig : MultiSortedSig) : Monad sortToC.
Proof.
use Monad_from_hss.
- apply BCsortToC.
- apply (MultiSortedSigToSignature sig).
- apply MultiSortedSigToHSS.
Defined.

End monad.
End MBindingSig.

Section MBindingSigMonadHSET.

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

Let sortToSet : category := [path_pregroupoid sort Hsort, HSET].

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

Definition hat_functorSet : sort → HSET ⟶ sortToSet :=
  hat_functor sort (isofhlevelssnset 1 _ (setproperty sort)) HSET CoproductsHSET.

Definition sorted_option_functorSet : sort → sortToSet ⟶ sortToSet :=
  sorted_option_functor _ (isofhlevelssnset 1 _ (setproperty sort)) HSET
                        TerminalHSET BinCoproductsHSET CoproductsHSET.

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

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

End MBindingSigMonadHSET.