Library UniMath.SubstitutionSystems.BindingSigToMonad

Definition of binding signatures (BindingSig) and translation from from binding signatures to monads (BindingSigToMonad). This is defined in multiple steps:
Written by: Anders Mörtberg, 2016

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Combinatorics.Lists.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
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.FunctorCategory.
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.Limits.
Require Import UniMath.CategoryTheory.Categories.HSET.Colimits.
Require Import UniMath.CategoryTheory.Categories.HSET.Structures.

Require Import UniMath.SubstitutionSystems.Signatures.
Require Import UniMath.SubstitutionSystems.SignatureExamples.
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.

Local Open Scope cat.

Local Notation "[ C , D ]" := (functor_category C D).
Local Notation "'chain'" := (diagram nat_graph).

Definition of binding signatures

Section BindingSig.

A binding signature is a collection of lists of natural numbers indexed by types I
Definition BindingSig : UU := ∑ (I : UU) (h : isaset I), I → list nat.

Definition BindingSigIndex : BindingSig -> UU := pr1.
Definition BindingSigIsaset (s : BindingSig) : isaset (BindingSigIndex s) :=
  pr1 (pr2 s).
Definition BindingSigMap (s : BindingSig) : BindingSigIndex s -> list nat :=
  pr2 (pr2 s).

Definition make_BindingSig {I : UU} (h : isaset I) (f : I -> list nat) : BindingSig := (I,,h,,f).

Sum of binding signatures
Definition SumBindingSig : BindingSig -> BindingSig -> BindingSig.
Show proof.
intros s1 s2.
use tpair.
- apply (BindingSigIndex s1 ⨿ BindingSigIndex s2).
- use tpair.
  + apply (isasetcoprod _ _ (BindingSigIsaset s1) (BindingSigIsaset s2)).
  + induction 1 as [i|i]; [ apply (BindingSigMap s1 i) | apply (BindingSigMap s2 i) ].

End BindingSig.

Translation from a binding signature to a monad

          S : BindingSig
      |-> functor(S) : functor [C,C] [C,C]
      |-> Initial (Id + functor(S))
      |-> I := Initial (HSS(func(S), θ)
      |-> M := Monad_from_HSS(I)
Section BindingSigToMonad.

Context {C : category}.

Local Notation "'[C,C]'" := (functor_category C C).

Form " o option^n" and return Id if n = 0
Definition precomp_option_iter (BCC : BinCoproducts C) (TC : Terminal C) (n : nat) : functor [C,C] [C,C].
Show proof.
induction n as [|n IHn].
- apply functor_identity.
- apply (pre_composition_functor _ _ _ (iter_functor1 _ (option_functor BCC TC) n)).

Lemma is_omega_cocont_precomp_option_iter
  (BCC : BinCoproducts C) (TC : Terminal C)
  (CLC : Colims_of_shape nat_graph C) (n : nat) :
  is_omega_cocont (precomp_option_iter BCC TC n).
Show proof.
destruct n; simpl.
- apply is_omega_cocont_functor_identity.
- apply is_omega_cocont_pre_composition_functor, CLC.

Definition precomp_option_iter_Signature (BCC : BinCoproducts C)
  (TC : Terminal C) (n : nat) : Signature C C C.
Show proof.
  use tpair.
  - exact (precomp_option_iter BCC TC n).
  - destruct n; simpl.
    + apply θ_functor_identity.
    + exact (pr2 (θ_from_δ_Signature C _ (DL_iter_functor1 C (option_functor BCC TC) (option_DistributiveLaw C TC BCC) n))).

Local Lemma functor_in_precomp_option_iter_Signature_ok (BCC : BinCoproducts C)
      (TC : Terminal C) (n : nat) : Signature_Functor (precomp_option_iter_Signature BCC TC n) = precomp_option_iter BCC TC n.
Show proof.
apply idpath.

Context (BPC : BinProducts C) (BCC : BinCoproducts C).

nat to a Signature
Definition Arity_to_Signature (TC : Terminal C) (xs : list nat) : Signature C C C :=
  foldr1_map (BinProduct_of_Signatures _ _ _ BPC)
         (ConstConstSignature C C C (TerminalObject TC))
         (precomp_option_iter_Signature BCC TC) xs.

Let BPC2 BPC := BinProducts_functor_precat C C BPC.
Let constprod_functor1 := constprod_functor1 (BPC2 BPC).

The H assumption follows directly if C,C has exponentials
Lemma is_omega_cocont_Arity_to_Signature
  (TC : Terminal C) (CLC : Colims_of_shape nat_graph C)
  (H : ∏ (F : [C,C]), is_omega_cocont (constprod_functor1 F))
  (xs : list nat) :
  is_omega_cocont (Arity_to_Signature TC xs).
Show proof.
  refine (foldr1_map_ind_nodep (BinProduct_of_Signatures _ _ _ BPC) _ _ is_omega_cocont _ _ _ xs).
  - apply is_omega_cocont_constant_functor.
  - intro n. apply is_omega_cocont_precomp_option_iter, CLC.
  - intros m sig Hyp.
    apply is_omega_cocont_BinProduct_of_Signatures.
    + apply is_omega_cocont_precomp_option_iter, CLC.
    + exact Hyp.
    + exact BPC.
    + exact H.

Binding signature to a signature with strength

Definition BindingSigToSignature (TC : Terminal C)
  (sig : BindingSig) (CC : Coproducts (BindingSigIndex sig) C) :
  Signature C C C.
Show proof.
  apply (Sum_of_Signatures (BindingSigIndex sig)).
  - apply CC.
  - intro i; apply (Arity_to_Signature TC (BindingSigMap sig i)).

Lemma is_omega_cocont_BindingSigToSignature
  (TC : Terminal C) (CLC : Colims_of_shape nat_graph C)
  (HF : ∏ (F : [C,C]), is_omega_cocont (constprod_functor1 F))
  (sig : BindingSig) (CC : Coproducts (BindingSigIndex sig) C) :
  is_omega_cocont (BindingSigToSignature TC sig CC).
Show proof.
  unfold BindingSigToSignature.
  apply is_omega_cocont_Sum_of_Signatures.
  now intro i; apply is_omega_cocont_Arity_to_Signature, HF.

Let Id_H := Id_H C BCC.

Construction of initial algebra for a signature with strength

Definition SignatureInitialAlgebra
  (IC : Initial C) (CLC : Colims_of_shape nat_graph C)
  (H : Presignature C C C) (Hs : is_omega_cocont H) :
  Initial (FunctorAlg (Id_H H)).
Show proof.
use colimAlgInitial.
- apply (Initial_functor_precat _ _ IC).
- apply (is_omega_cocont_Id_H _ _ _ Hs).
- apply ColimsFunctorCategory_of_shape, CLC.

Construction of datatype specified by a binding signature

Definition DatatypeOfBindingSig
  (IC : Initial C) (TC : Terminal C) (CLC : Colims_of_shape nat_graph C)
  (HF : ∏ (F : [C,C]), is_omega_cocont (constprod_functor1 F))
  (sig : BindingSig) (CC : Coproducts (BindingSigIndex sig) C) :
  Initial (FunctorAlg (Id_H (Presignature_Signature(BindingSigToSignature TC sig CC)))).
Show proof.
apply SignatureInitialAlgebra; trivial.
now apply is_omega_cocont_BindingSigToSignature.

Let HSS := @hss_category C BCC.

Let InitialHSS
  (IC : Initial C) (CLC : Colims_of_shape nat_graph C)
  (H : Presignature C C C) (Hs : is_omega_cocont H) :
  Initial (HSS H).
Show proof.
apply InitialHSS; assumption.

Signature with strength and initial algebra to a HSS

Definition SignatureToHSS
  (IC : Initial C) (CLC : Colims_of_shape nat_graph C)
  (H : Presignature C C C) (Hs : is_omega_cocont H) :
  HSS H.
Show proof.
now apply InitialHSS; assumption.

The above HSS is initial
Definition SignatureToHSSisInitial
  (IC : Initial C) (CLC : Colims_of_shape nat_graph C)
  (H : Presignature C C C) (Hs : is_omega_cocont H) :
  isInitial _ (SignatureToHSS IC CLC H Hs).
Show proof.
now unfold SignatureToHSS; destruct InitialHSS.

Let Monad_from_hss (H : Signature C C C) : HSS H → Monad C.
Show proof.
exact (Monad_from_hss _ BCC H).

Function from binding signatures to monads

Definition BindingSigToMonad
  (TC : Terminal C) (IC : Initial C) (CLC : Colims_of_shape nat_graph C)
  (HF : ∏ (F : [C,C]), is_omega_cocont (constprod_functor1 F))
  (sig : BindingSig)
  (CC : Coproducts (BindingSigIndex sig) C) :
  Monad C.
Show proof.
use Monad_from_hss.
- apply (BindingSigToSignature TC sig CC).
- apply (SignatureToHSS IC CLC).
  apply (is_omega_cocont_BindingSigToSignature TC CLC HF _ _).

End BindingSigToMonad.

Specialized versions of some of the above functions for HSET

Section BindingSigToMonadHSET.

Binding signature to signature with strength for HSET

Definition BindingSigToSignatureHSET (sig : BindingSig) : Signature HSET HSET HSET.
Show proof.
use BindingSigToSignature.
- apply BinProductsHSET.
- apply BinCoproductsHSET.
- apply TerminalHSET.
- apply sig.
- apply CoproductsHSET, (BindingSigIsaset sig).

Lemma is_omega_cocont_BindingSigToSignatureHSET (sig : BindingSig) :
  is_omega_cocont (BindingSigToSignatureHSET sig).
Show proof.
apply is_omega_cocont_Sum_of_Signatures.
intro i; apply is_omega_cocont_Arity_to_Signature.
+ apply ColimsHSET_of_shape.
+ intros F.
  apply is_omega_cocont_constprod_functor1.
  apply Exponentials_functor_HSET.

Construction of initial algebra for a signature with strength for HSET

Definition SignatureInitialAlgebraHSET (s : Presignature HSET _ _) (Hs : is_omega_cocont s) :
  Initial (FunctorAlg (Id_H _ BinCoproductsHSET s)).
Show proof.
apply SignatureInitialAlgebra; try assumption.
- apply InitialHSET.
- apply ColimsHSET_of_shape.

Binding signature to a monad for HSET

Definition BindingSigToMonadHSET : BindingSig → Monad HSET.
Show proof.
intros sig; use (BindingSigToMonad _ _ _ _ _ _ sig).
- apply BinProductsHSET.
- apply BinCoproductsHSET.
- apply TerminalHSET.
- apply InitialHSET.
- apply ColimsHSET_of_shape.
- intros F.
  apply is_omega_cocont_constprod_functor1.
  apply Exponentials_functor_HSET.
- apply CoproductsHSET.
  apply BindingSigIsaset.

End BindingSigToMonadHSET.