Library UniMath.SubstitutionSystems.MultiSorted

This file contains a fomalization of multisorted binding signatures:
Written by: Anders Mörtberg, 2016. The formalization follows a note written by Benedikt Ahrens and Ralph Matthes, and is also inspired by discussions with them and Vladimir Voevodsky.
Strength calculation added by Ralph Matthes, 2017.
In the end of the file there is a module with an alternative version using X,SET instead of SET/X. There is no proof that the functor we obtain using this approach is omega-cocontinuous yet.

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.Isos.
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.limits.
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.limits.pullbacks.
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.Slice.
Require Import UniMath.CategoryTheory.categories.HSET.Structures.
Require Import UniMath.CategoryTheory.HorizontalComposition.
Require Import UniMath.CategoryTheory.slicecat.

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.Notation.
Local Open Scope subsys.
Require Import UniMath.SubstitutionSystems.SignatureExamples.
Require Import UniMath.SubstitutionSystems.BindingSigToMonad.
Require Import UniMath.SubstitutionSystems.MonadsMultiSorted.

Local Open Scope cat.

Local Notation "C / X" := (slicecat_ob C X).
Local Notation "C / X" := (slice_precat_data C X).
Local Notation "C / X" := (slice_precat C X (homset_property C)).
Local Notation "C / X ⟦ a , b ⟧" := (slicecat_mor C X a b) (at level 50, format "C / X ⟦ a , b ⟧").

Arguments post_composition_functor {_ _ _} _ _ _.
Arguments pre_composition_functor {_ _ _} _ _ _.
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

Definition of multi sorted 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).

Construction of an endofunctor on SET/sort,SET/sort from a multisorted signature

Section functor.

Local Definition proj_fun (s : sort) : SET / sort SET :=
  λ p, hfiber_hSet (pr2 p) s.

Definition proj_functor (s : sort) : functor (SET / sort) SET.
use tpair.
- (proj_fun s).
  intros X Y f p.
   (pr1 f (pr1 p)).
  abstract (now induction f as [h hh]; induction p as [x hx]; simpl in *; rewrite <- hx, hh).
- abstract (split; [intros X|intros X Y Z f g];
            apply funextsec; intro p; apply subtypePath; trivial;
            intros x; apply setproperty).

The left adjoint to the proj_functor
Definition hat_functor (t : sort) : functor SET (SET / sort).
use tpair.
- use tpair.
  + intro A; apply (A,,λ _, t).
  + intros A B f; apply (tpair _ f), idpath.
- abstract (now split; [intros A|intros A B C f g];
            apply subtypePath; try (intro x; apply has_homsets_HSET)).

Local Definition constHSET_slice := constHSET_slice sort.

Local Definition sorted_option_functor := sorted_option_functor sort.

Sorted option functor for lists (also called option in the note)
Local Definition option_list (xs : list sort) : functor (SET / sort) (SET / sort).
use (foldr1 (λ F G, F G) (functor_identity _) (map sorted_option_functor xs)).

Define a functor
F^(l,t)(X) := proj_functor(t) ∘ X ∘ option_functor(l)
if l is nonempty and
F^(l,t)(X) := proj_functor(t) ∘ X
Definition exp_functor (lt : list sort × sort) :
  functor [SET_over_sort,SET_over_sort] [SET_over_sort,SET].
induction lt as [l t].
use (list_ind _ _ _ l); clear l.
- exact (post_composition_functor _ _ (proj_functor t)).
- intros s l _; simpl.
  eapply functor_composite.
  + exact (pre_composition_functor hs hs (option_list (cons s l))).
  + exact (post_composition_functor _ has_homsets_HSET (proj_functor t)).

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.
The function from multisorted signatures to functors

Construction of the strength for the endofunctor on SET/sort,SET/sort derived from a

multisorted signature
Section strength.

Local Definition DL_sorted_option_functor (s : sort) :
  DistributiveLaw _ hs (sorted_option_functor s) :=
    genoption_DistributiveLaw _ hs (constHSET_slice s)(BinCoproducts_HSET_slice sort).

Local Definition DL_option_list (xs : list sort) :
  DistributiveLaw _ hs (option_list xs).
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))).

Local Definition Sig_exp_functor (lt : list sort × sort) :
  Signature _ hs _ has_homsets_HSET _ hs.
(exp_functor lt).
induction lt as [l t].
induction l as [[|n] xs].
+ induction xs.
  exact (pr2 (Gθ_Signature _ _ (IdSignature _ _ _ _) (proj_functor t))).
+ induction n as [|n IH].
  × induction xs as [m []].
    set (Sig_option_list := θ_from_δ_Signature (DL_option_list (cons m (0,,tt)))).
    exact (pr2 (Gθ_Signature _ _ Sig_option_list (proj_functor t))).
  × induction xs as [m xs].
    set (Sig_option_list := θ_from_δ_Signature (DL_option_list (cons m (S n,,xs)))).
    exact (pr2 (Gθ_Signature _ _ Sig_option_list (proj_functor t))).

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

Local Definition Sig_exp_functor_list (xs : list (list sort × sort)) :
  Signature _ hs _ has_homsets_HSET _ hs.
(exp_functor_list xs).
induction xs as [[|n] xs].
- induction xs.
  exact (pr2 (ConstConstSignature SET_over_sort SET SET_over_sort TerminalHSET)).
- 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))))).

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.
apply idpath.

Local Definition Sig_hat_exp_functor_list (xst : list (list sort × sort) × sort) :
  Signature _ hs _ hs _ hs.
apply (Gθ_Signature _ _ (Sig_exp_functor_list (pr1 xst)) (hat_functor (pr2 xst))).

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.
apply idpath.

Definition MultiSortedSigToSignature (M : MultiSortedSig) : Signature _ hs _ hs _ hs.
set (Hyps := λ (op : ops M), Sig_hat_exp_functor_list (arity M op)).
use (Sum_of_Signatures (ops M) _ _ _ Hyps).
apply Coproducts_slice_precat, CoproductsHSET, setproperty.

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

End strength.

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

Section omega_cocont.

The proj functor is naturally isomorphic to the following functor which is a left adjoint:
Local Definition proj_functor' (s : sort) : functor (SET / sort) SET :=
     (constprod_functor1 (BinProducts_HSET_slice sort) (constHSET_slice s))
     (slicecat_to_cat has_homsets_HSET sort).

Local Lemma nat_trans_proj_functor (s : sort) : nat_trans (proj_functor' s) (proj_functor s).
use make_nat_trans.
- simpl; intros x H.
   (pr2 (pr1 H)).
  apply (!pr2 H).
- intros x y f.
  apply funextsec; intro w.
  apply subtypePath; trivial.
  intro z; apply setproperty.

Local Lemma is_iso_nat_trans_proj_functor (s : sort) :
  @is_iso [SET/sort,SET] _ _ (nat_trans_proj_functor s).
use is_iso_qinv.
+ use make_nat_trans.
  - simpl; intros x xy.
     (tt,,pr1 xy).
    apply (!pr2 xy).
  - abstract (intros X Y f; apply funextsec; intros x;
              apply subtypePath; trivial; intros w; apply setproperty).
+ abstract (split;
  [ apply subtypePath; [intros x; apply isaprop_is_nat_trans, has_homsets_HSET|];
    apply funextsec; intro x; apply funextsec; intro y; cbn;
    now rewrite pathsinv0inv0; induction y as [y' y3]; induction y' as [y'' y2]; induction y''
  | apply (nat_trans_eq has_homsets_HSET); simpl; intros x;
    apply funextsec; intros z; simpl in *;
    now apply subtypePath; trivial; intros w; apply setproperty]).

Local Lemma is_left_adjoint_proj_functor' (s : sort) : is_left_adjoint (proj_functor' s).
use is_left_adjoint_functor_composite.
- apply Exponentials_HSET_slice.
- apply is_left_adjoint_slicecat_to_cat_HSET.

Local Lemma is_left_adjoint_proj_functor (s : sort) : is_left_adjoint (proj_functor s).
apply (is_left_adjoint_iso _ _ _ (_,,is_iso_nat_trans_proj_functor s)).
apply is_left_adjoint_proj_functor'.

Local Lemma is_omega_cocont_post_comp_proj (s : sort) :
  is_omega_cocont (@post_composition_functor (SET/sort) _ _ hs has_homsets_HSET (proj_functor s)).
apply is_omega_cocont_post_composition_functor.
apply is_left_adjoint_proj_functor.

The hat_functor is left adjoint to proj_functor
Local Lemma is_left_adjoint_hat (s : sort) : is_left_adjoint (hat_functor s).
(proj_functor s).
use make_are_adjoints.
+ use make_nat_trans.
  - intros X; simpl; intros x; apply (x,,idpath s).
  - intros X Y f; simpl; apply funextsec; intro x; cbn.
    now apply subtypePath; trivial; intros y; apply setproperty.
+ use make_nat_trans.
  - intros X; simpl in ×.
    use tpair; simpl.
    × intros H; apply (pr1 H).
    × abstract (apply funextsec; intro x; apply (! pr2 x)).
  - now intros X Y f; apply (eq_mor_slicecat has_homsets_HSET).
+ split.
  - now intros X; apply (eq_mor_slicecat has_homsets_HSET).
  - intros X; apply funextsec; intro x.
    now apply subtypePath; trivial; intros x'; apply setproperty.

Local Lemma is_omega_cocont_exp_functor (a : list sort × sort)
  (H : Colims_of_shape nat_graph SET_over_sort) :
  is_omega_cocont (exp_functor a).
induction a as [xs t].
induction xs as [[|n] xs].
- induction xs.
  apply is_omega_cocont_post_comp_proj.
- induction n as [|n].
  + induction xs as [m []].
    use is_omega_cocont_functor_composite.
    × apply functor_category_has_homsets.
    × apply is_omega_cocont_pre_composition_functor, H.
    × apply is_omega_cocont_post_comp_proj.
  + induction xs as [m k]; simpl.
    use (@is_omega_cocont_functor_composite _ _ _ _ ( (option_list _))).
    × apply (functor_category_has_homsets (SET / sort) HSET has_homsets_HSET).
    × apply is_omega_cocont_pre_composition_functor, H.
    × apply is_omega_cocont_post_comp_proj.

Local Lemma is_omega_cocont_exp_functor_list (xs : list (list sort × sort))
  (H : Colims_of_shape nat_graph SET_over_sort) :
  is_omega_cocont (exp_functor_list xs).
induction xs as [[|n] xs].
- induction xs.
  apply is_omega_cocont_constant_functor, functor_category_has_homsets.
- induction n as [|n IHn].
  + induction xs as [m []].
    apply is_omega_cocont_exp_functor, H.
  + induction xs as [m [k xs]].
    apply is_omega_cocont_BinProduct_of_functors; try apply homset_property.
    × apply BinProducts_functor_precat, BinProducts_slice_precat, PullbacksHSET.
    × apply is_omega_cocont_constprod_functor1; try apply functor_category_has_homsets.
      apply Exponentials_functor_HSET, homset_property.
    × apply is_omega_cocont_exp_functor, H.
    × apply (IHn (k,,xs)).

Local Lemma is_omega_cocont_post_comp_hat_functor (s : sort) :
  is_omega_cocont (@post_composition_functor SET_over_sort _ _
       (homset_property SET) hs (hat_functor s)).
apply is_omega_cocont_post_composition_functor, is_left_adjoint_hat.

Local Lemma is_omega_cocont_hat_exp_functor_list (xst : list (list sort × sort) × sort)
  (H : Colims_of_shape nat_graph SET_over_sort) :
  is_omega_cocont (hat_exp_functor_list xst).
apply is_omega_cocont_functor_composite.
+ apply functor_category_has_homsets.
+ apply is_omega_cocont_exp_functor_list, H.
+ apply is_omega_cocont_post_comp_hat_functor.

The functor obtained from a multisorted binding signature is omega-cocontinuous

Construction of a monad from a multisorted signature

Function from multisorted binding signatures to monads

Definition MultiSortedSigToMonad (sig : MultiSortedSig) : Monad (SET / sort).
use Monad_from_hss.
- apply hs.
- apply BinCoproducts_HSET_slice.
- apply (MultiSortedSigToSignature sig).
- apply MultiSortedSigToHSS.

End monad.
End MBindingSig.

Alternative version using X,SET instead of SET/X below. There is no proof that the functor we obtain using this approach is omega-cocontinuous yet.
Require UniMath.CategoryTheory.categories.StandardCategories.
Require UniMath.CategoryTheory.Adjunctions.Examples.

Module alt.

Import UniMath.CategoryTheory.Groupoids.
Import UniMath.CategoryTheory.categories.StandardCategories.
Import UniMath.CategoryTheory.Adjunctions.Examples.

Definition of multisorted binding signatures

Section MBindingSig.

Variables (sort : UU) (eq : isdeceq sort). Variables (C : category) (BP : BinProducts C) (BC : BinCoproducts C) (TC : Terminal C).

Define the discrete category of sorts
This represents "sort → C"
Let sortToC : category := [sort_cat,C].

Local Lemma has_homsets_sortToC : has_homsets sortToC.
apply homset_property.

Local Definition BinProductsSortToCToC : BinProducts [sortToC,C].
apply (BinProducts_functor_precat _ _ BP).

Local Definition make_sortToC (f : sort C) : sortToC := functor_path_pregroupoid f.

Local Definition proj_gen_fun (D : precategory) (E : category) (d : D) : functor [D,E] E.
use tpair.
+ use tpair.
  - intro f; apply (pr1 f d).
  - simpl; intros a b f; apply (f d).
+ abstract (split; [intro f; apply idpath|intros f g h fg gh; apply idpath]).

Local Definition proj_gen {D : precategory} {E : category} : functor D [[D,E],E].
use tpair.
+ use tpair.
  - apply proj_gen_fun.
  - intros d1 d2 f.
    use tpair.
    × red; simpl; intro F; apply (# F f).
    × abstract (intros F G α; simpl in *; apply pathsinv0, (nat_trans_ax α d1 d2 f)).
+ abstract (split;
  [ intros F; simpl; apply nat_trans_eq; [apply homset_property|]; intro G; simpl; apply functor_id
  | intros F G H α β; simpl; apply nat_trans_eq; [apply homset_property|];
    intro γ; simpl; apply functor_comp ]).

Given a sort s this applies the sortToC to s and returns C
Definition projSortToC (s : sort) : functor sortToC C.
apply proj_gen_fun.
apply s.

Definition of multi sorted signatures
Definition MultiSortedSig : UU :=
   (s : sort), (I : UU), (I list (list sort × sort)).
Definition indices (M : MultiSortedSig) : sort UU := λ s, pr1 (M s).

Definition args (M : MultiSortedSig) (s : sort) : indices M s list (list sort × sort) :=
  pr2 (M s).

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

Local Definition option_fun : sort sortToC sortToC.
intros s f.
apply make_sortToC; intro t.
induction (eq s t) as [H|H].
- apply (pr1 f t 1).
- apply (pr1 f t).

Local Definition option_functor_data (s : sort) : functor_data sortToC sortToC.
use tpair.
+ apply (option_fun s).
+ cbn. intros F G α.
  use tpair.
  × red; simpl; intro t.
    induction (eq s t) as [p|p]; simpl; clear p.
    { apply (BinCoproductOfArrows _ _ _ (α t) (identity _)). }
    { apply α. }
  × abstract (now intros t1 t2 []; cbn; induction (eq s t1); simpl; rewrite id_left, id_right).
Local Lemma is_functor_option_functor s : is_functor (option_functor_data s).
+ intros F; apply (nat_trans_eq hsC); intro t; simpl.
  induction (eq s t) as [p|p]; trivial; simpl; clear p.
  now apply pathsinv0, BinCoproductArrowUnique; rewrite id_left, id_right.
+ intros F G H αFG αGH; apply (nat_trans_eq hsC); intro t; simpl.
  induction (eq s t) as [p|p]; trivial; simpl; clear p.
  apply pathsinv0; eapply pathscomp0; [apply precompWithBinCoproductArrow|].
  rewrite !id_left; apply BinCoproductArrowUnique.
  × now rewrite BinCoproductIn1Commutes, assoc.
  × now rewrite BinCoproductIn2Commutes, id_left.
Local Definition option_functor (s : sort) : functor sortToC sortToC :=
  tpair _ _ (is_functor_option_functor s).

Local Definition option_list (xs : list sort) : functor sortToC sortToC.
use (foldr _ _ xs).
+ intros s F.
  apply (functor_composite (option_functor s) F).
+ apply functor_identity.

Local Lemma exp_functor (a : list sort × sort) : functor [sortToC,sortToC] [sortToC,C].
eapply functor_composite.
- apply (pre_composition_functor has_homsets_sortToC _ (option_list (pr1 a))).
- apply post_composition_functor, (projSortToC (pr2 a)).

Local Definition exp_functors (xs : list (list sort × sort)) :
  functor [sortToC,sortToC] [sortToC,C].
set (XS := map exp_functor xs).
set (T := constant_functor [sortToC,sortToC] [sortToC,C]
                           (constant_functor sortToC C TC)).
apply (foldr1 (λ F G, BinProduct_of_functors BinProductsSortToCToC F G) T XS).

Local Definition MultiSortedSigToFunctor_helper1 (C1 D E1 : precategory) (E2 : category)
  : functor [E1,[C1,[D,E2]]] [E1,[D,[C1,E2]]].
eapply post_composition_functor.
apply functor_cat_swap.

Local Definition MultiSortedSigToFunctor_helper (C1 D E1 : precategory) (E2 : category) :
  functor [E1,[C1,[D,E2]]] [C1,[D,[E1,E2]]].
eapply (functor_composite (functor_cat_swap _ _ _)).
apply MultiSortedSigToFunctor_helper1.

Local Definition MultiSortedSigToFunctor_fun (M : MultiSortedSig) (CC : s, Coproducts (indices M s) C)
  : [sort_cat, [[sortToC, sortToC], [sortToC, C]]].
  apply functor_path_pregroupoid; intro s.
  use (coproduct_of_functors (indices M s)).
  + apply Coproducts_functor_precat, CC.
  + intros y; apply (exp_functors (args M s y)).

The functor constructed from a multisorted binding signature