Library UniMath.SubstitutionSystems.BindingSigToMonad
- Binding signature to a signature with strength (BindingSigToSignature)
- Construction of initial algebra for a signature with strength (SignatureInitialAlgebra)
- Signature with strength and initial algebra to a HSS (SignatureToHSS)
- Construction of a monad from a HSS (Monad_from_hss in MonadsFromSubstitutionSystems.v)
- Composition of these maps to get a function from binding signatures to monads (BindingSigToMonad)
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Combinatorics.Lists.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.functor_categories.
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.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 , hsD ]" := (functor_precategory C D hsD).
Local Notation "'chain'" := (diagram nat_graph).
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 mkBindingSig {I : UU} (h : isaset I) (f : I → list nat) : BindingSig := (I,,h,,f).
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 mkBindingSig {I : UU} (h : isaset I) (f : I → list nat) : BindingSig := (I,,h,,f).
Sum of binding signatures
Definition SumBindingSig : BindingSig → BindingSig → BindingSig.
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) ].
Defined.
End BindingSig.
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) ].
Defined.
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 : precategory} (hsC : has_homsets C).
Local Notation "'[C,C]'" := (functor_precategory C C hsC).
Local Definition has_homsets_C2 : has_homsets [C,C].
Proof.
apply functor_category_has_homsets.
Defined.
Context {C : precategory} (hsC : has_homsets C).
Local Notation "'[C,C]'" := (functor_precategory C C hsC).
Local Definition has_homsets_C2 : has_homsets [C,C].
Proof.
apply functor_category_has_homsets.
Defined.
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].
Proof.
induction n as [|n IHn].
- apply functor_identity.
- apply (pre_composition_functor _ _ _ hsC _ (iter_functor1 _ (option_functor BCC TC) n)).
Defined.
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).
Proof.
destruct n; simpl.
- apply (is_omega_cocont_functor_identity has_homsets_C2).
- apply is_omega_cocont_pre_composition_functor, CLC.
Defined.
Definition precomp_option_iter_Signature (BCC : BinCoproducts C)
(TC : Terminal C) (n : nat) : Signature C hsC C hsC.
Proof.
use tpair.
- exact (precomp_option_iter BCC TC n).
- destruct n; simpl.
+ apply θ_functor_identity.
+ exact (pr2 (θ_from_δ_Signature C hsC _ (DL_iter_functor1 C hsC (option_functor BCC TC) (option_DistributiveLaw C hsC TC BCC) n))).
Defined.
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.
Proof.
apply idpath.
Qed.
Context (BPC : BinProducts C) (BCC : BinCoproducts C).
Proof.
induction n as [|n IHn].
- apply functor_identity.
- apply (pre_composition_functor _ _ _ hsC _ (iter_functor1 _ (option_functor BCC TC) n)).
Defined.
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).
Proof.
destruct n; simpl.
- apply (is_omega_cocont_functor_identity has_homsets_C2).
- apply is_omega_cocont_pre_composition_functor, CLC.
Defined.
Definition precomp_option_iter_Signature (BCC : BinCoproducts C)
(TC : Terminal C) (n : nat) : Signature C hsC C hsC.
Proof.
use tpair.
- exact (precomp_option_iter BCC TC n).
- destruct n; simpl.
+ apply θ_functor_identity.
+ exact (pr2 (θ_from_δ_Signature C hsC _ (DL_iter_functor1 C hsC (option_functor BCC TC) (option_DistributiveLaw C hsC TC BCC) n))).
Defined.
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.
Proof.
apply idpath.
Qed.
Context (BPC : BinProducts C) (BCC : BinCoproducts C).
nat to a Signature
Definition Arity_to_Signature (TC : Terminal C) (xs : list nat) : Signature C hsC C hsC :=
foldr1 (BinProduct_of_Signatures _ _ _ _ BPC)
(ConstConstSignature (category_pair C hsC) (category_pair C hsC) (TerminalObject TC))
(map (precomp_option_iter_Signature BCC TC) xs).
Let BPC2 BPC := BinProducts_functor_precat C _ BPC hsC.
Let constprod_functor1 := constprod_functor1 (BPC2 BPC).
foldr1 (BinProduct_of_Signatures _ _ _ _ BPC)
(ConstConstSignature (category_pair C hsC) (category_pair C hsC) (TerminalObject TC))
(map (precomp_option_iter_Signature BCC TC) xs).
Let BPC2 BPC := BinProducts_functor_precat C _ BPC hsC.
Let constprod_functor1 := constprod_functor1 (BPC2 BPC).
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).
Proof.
destruct xs as [[|n] xs].
- destruct xs; apply (is_omega_cocont_constant_functor has_homsets_C2).
- induction n as [|n IHn].
+ destruct xs as [m []]; simpl.
unfold Arity_to_Signature.
apply is_omega_cocont_precomp_option_iter, CLC.
+ destruct xs as [m [k xs]].
apply is_omega_cocont_BinProduct_of_Signatures.
× apply is_omega_cocont_precomp_option_iter, CLC.
× apply (IHn (k,,xs)).
× assumption.
× intro x; apply (H x).
Defined.
(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).
Proof.
destruct xs as [[|n] xs].
- destruct xs; apply (is_omega_cocont_constant_functor has_homsets_C2).
- induction n as [|n IHn].
+ destruct xs as [m []]; simpl.
unfold Arity_to_Signature.
apply is_omega_cocont_precomp_option_iter, CLC.
+ destruct xs as [m [k xs]].
apply is_omega_cocont_BinProduct_of_Signatures.
× apply is_omega_cocont_precomp_option_iter, CLC.
× apply (IHn (k,,xs)).
× assumption.
× intro x; apply (H x).
Defined.
Definition BindingSigToSignature (TC : Terminal C)
(sig : BindingSig) (CC : Coproducts (BindingSigIndex sig) C) :
Signature C hsC C hsC.
Proof.
apply (Sum_of_Signatures (BindingSigIndex sig)).
- apply CC.
- intro i; apply (Arity_to_Signature TC (BindingSigMap sig i)).
Defined.
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).
Proof.
apply is_omega_cocont_Sum_of_Signatures.
now intro i; apply is_omega_cocont_Arity_to_Signature, HF.
Defined.
Let Id_H := Id_H C hsC BCC.
Let FunctorAlg F := FunctorAlg F has_homsets_C2.
(sig : BindingSig) (CC : Coproducts (BindingSigIndex sig) C) :
Signature C hsC C hsC.
Proof.
apply (Sum_of_Signatures (BindingSigIndex sig)).
- apply CC.
- intro i; apply (Arity_to_Signature TC (BindingSigMap sig i)).
Defined.
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).
Proof.
apply is_omega_cocont_Sum_of_Signatures.
now intro i; apply is_omega_cocont_Arity_to_Signature, HF.
Defined.
Let Id_H := Id_H C hsC BCC.
Let FunctorAlg F := FunctorAlg F has_homsets_C2.
Definition SignatureInitialAlgebra
(IC : Initial C) (CLC : Colims_of_shape nat_graph C)
(H : Signature C hsC C hsC) (Hs : is_omega_cocont H) :
Initial (FunctorAlg (Id_H H)).
Proof.
use colimAlgInitial.
- apply (Initial_functor_precat _ _ IC).
- apply (is_omega_cocont_Id_H _ _ _ _ Hs).
- apply ColimsFunctorCategory_of_shape, CLC.
Defined.
(IC : Initial C) (CLC : Colims_of_shape nat_graph C)
(H : Signature C hsC C hsC) (Hs : is_omega_cocont H) :
Initial (FunctorAlg (Id_H H)).
Proof.
use colimAlgInitial.
- apply (Initial_functor_precat _ _ IC).
- apply (is_omega_cocont_Id_H _ _ _ _ Hs).
- apply ColimsFunctorCategory_of_shape, CLC.
Defined.
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 (BindingSigToSignature TC sig CC))).
Proof.
apply SignatureInitialAlgebra; trivial.
now apply is_omega_cocont_BindingSigToSignature.
Defined.
Let HSS := @hss_precategory C hsC BCC.
Let InitialHSS
(IC : Initial C) (CLC : Colims_of_shape nat_graph C)
(H : Signature C hsC C hsC) (Hs : is_omega_cocont H) :
Initial (HSS H).
Proof.
apply InitialHSS; assumption.
Defined.
(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 (BindingSigToSignature TC sig CC))).
Proof.
apply SignatureInitialAlgebra; trivial.
now apply is_omega_cocont_BindingSigToSignature.
Defined.
Let HSS := @hss_precategory C hsC BCC.
Let InitialHSS
(IC : Initial C) (CLC : Colims_of_shape nat_graph C)
(H : Signature C hsC C hsC) (Hs : is_omega_cocont H) :
Initial (HSS H).
Proof.
apply InitialHSS; assumption.
Defined.
Definition SignatureToHSS
(IC : Initial C) (CLC : Colims_of_shape nat_graph C)
(H : Signature C hsC C hsC) (Hs : is_omega_cocont H) :
HSS H.
Proof.
now apply InitialHSS; assumption.
Defined.
(IC : Initial C) (CLC : Colims_of_shape nat_graph C)
(H : Signature C hsC C hsC) (Hs : is_omega_cocont H) :
HSS H.
Proof.
now apply InitialHSS; assumption.
Defined.
The above HSS is initial
Definition SignatureToHSSisInitial
(IC : Initial C) (CLC : Colims_of_shape nat_graph C)
(H : Signature C hsC C hsC) (Hs : is_omega_cocont H) :
isInitial _ (SignatureToHSS IC CLC H Hs).
Proof.
now unfold SignatureToHSS; destruct InitialHSS.
Qed.
Let Monad_from_hss (H : Signature C hsC C hsC) : HSS H → Monad C.
Proof.
exact (Monad_from_hss _ _ BCC H).
Defined.
(IC : Initial C) (CLC : Colims_of_shape nat_graph C)
(H : Signature C hsC C hsC) (Hs : is_omega_cocont H) :
isInitial _ (SignatureToHSS IC CLC H Hs).
Proof.
now unfold SignatureToHSS; destruct InitialHSS.
Qed.
Let Monad_from_hss (H : Signature C hsC C hsC) : HSS H → Monad C.
Proof.
exact (Monad_from_hss _ _ BCC H).
Defined.
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.
Proof.
use Monad_from_hss.
- apply (BindingSigToSignature TC sig CC).
- apply (SignatureToHSS IC CLC).
apply (is_omega_cocont_BindingSigToSignature TC CLC HF _ _).
Defined.
End 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.
Proof.
use Monad_from_hss.
- apply (BindingSigToSignature TC sig CC).
- apply (SignatureToHSS IC CLC).
apply (is_omega_cocont_BindingSigToSignature TC CLC HF _ _).
Defined.
End BindingSigToMonad.
Section BindingSigToMonadHSET.
Local Definition has_homsets_HSET2 : has_homsets [HSET,HSET,has_homsets_HSET].
Proof.
apply functor_category_has_homsets.
Defined.
Local Definition has_homsets_HSET2 : has_homsets [HSET,HSET,has_homsets_HSET].
Proof.
apply functor_category_has_homsets.
Defined.
Definition BindingSigToSignatureHSET (sig : BindingSig) : Signature HSET has_homsets_HSET HSET has_homsets_HSET.
Proof.
use BindingSigToSignature.
- apply BinProductsHSET.
- apply BinCoproductsHSET.
- apply TerminalHSET.
- apply sig.
- apply CoproductsHSET, (BindingSigIsaset sig).
Defined.
Lemma is_omega_cocont_BindingSigToSignatureHSET (sig : BindingSig) :
is_omega_cocont (BindingSigToSignatureHSET sig).
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 _ has_homsets_HSET2).
apply Exponentials_functor_HSET, has_homsets_HSET.
Defined.
Proof.
use BindingSigToSignature.
- apply BinProductsHSET.
- apply BinCoproductsHSET.
- apply TerminalHSET.
- apply sig.
- apply CoproductsHSET, (BindingSigIsaset sig).
Defined.
Lemma is_omega_cocont_BindingSigToSignatureHSET (sig : BindingSig) :
is_omega_cocont (BindingSigToSignatureHSET sig).
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 _ has_homsets_HSET2).
apply Exponentials_functor_HSET, has_homsets_HSET.
Defined.
Definition SignatureInitialAlgebraHSET (s : Signature HSET has_homsets_HSET _ _) (Hs : is_omega_cocont s) :
Initial (FunctorAlg (Id_H _ _ BinCoproductsHSET s) has_homsets_HSET2).
Proof.
apply SignatureInitialAlgebra; try assumption.
- apply InitialHSET.
- apply ColimsHSET_of_shape.
Defined.
Initial (FunctorAlg (Id_H _ _ BinCoproductsHSET s) has_homsets_HSET2).
Proof.
apply SignatureInitialAlgebra; try assumption.
- apply InitialHSET.
- apply ColimsHSET_of_shape.
Defined.
Definition BindingSigToMonadHSET : BindingSig → Monad HSET.
Proof.
intros sig; use (BindingSigToMonad _ _ _ _ _ _ _ sig).
- apply has_homsets_HSET.
- apply BinProductsHSET.
- apply BinCoproductsHSET.
- apply TerminalHSET.
- apply InitialHSET.
- apply ColimsHSET_of_shape.
- intros F.
apply (is_omega_cocont_constprod_functor1 _ has_homsets_HSET2).
apply Exponentials_functor_HSET, has_homsets_HSET.
- apply CoproductsHSET.
apply BindingSigIsaset.
Defined.
End BindingSigToMonadHSET.
Proof.
intros sig; use (BindingSigToMonad _ _ _ _ _ _ _ sig).
- apply has_homsets_HSET.
- apply BinProductsHSET.
- apply BinCoproductsHSET.
- apply TerminalHSET.
- apply InitialHSET.
- apply ColimsHSET_of_shape.
- intros F.
apply (is_omega_cocont_constprod_functor1 _ has_homsets_HSET2).
apply Exponentials_functor_HSET, has_homsets_HSET.
- apply CoproductsHSET.
apply BindingSigIsaset.
Defined.
End BindingSigToMonadHSET.