From 134527ec34ffaa110cbab3a3db63dfc6e4419050 Mon Sep 17 00:00:00 2001 From: Ralph Matthes Date: Tue, 14 Feb 2017 16:02:27 +0100 Subject: [PATCH 1/7] define option_functor as instance of a generalized option functor generalized option functors are just the functors "a + _" and "_ + a" with arbitrary fixed a instead of a terminal object --- UniMath/CategoryTheory/limits/bincoproducts.v | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/UniMath/CategoryTheory/limits/bincoproducts.v b/UniMath/CategoryTheory/limits/bincoproducts.v index 412aeb914e..44cb7d7d67 100644 --- a/UniMath/CategoryTheory/limits/bincoproducts.v +++ b/UniMath/CategoryTheory/limits/bincoproducts.v @@ -941,16 +941,31 @@ Defined. End def_functor_pointwise_coprod. + +Section generalized_option_functors. + +Context {C : precategory} (CC : BinCoproducts C). + +(* The functors "a + _" and "_ + a" *) +Definition constcoprod_functor1 (a : C) : functor C C := + BinCoproduct_of_functors C C CC (constant_functor C C a) (functor_identity C). + +Definition constcoprod_functor2 (a : C) : functor C C := + BinCoproduct_of_functors C C CC (functor_identity C) (constant_functor C C a). + + Section option_functor. -Context {C : precategory} (CC : BinCoproducts C) (TC : Terminal C). +Context (TC : Terminal C). Let one : C := TerminalObject TC. Definition option_functor : functor C C := - BinCoproduct_of_functors C C CC (constant_functor _ _ one) (functor_identity C). + constcoprod_functor1 one. End option_functor. +End generalized_option_functors. + (** ** Construction of isBinCoproduct from an isomorphism to BinCoproduct. *) Section BinCoproduct_from_iso. From 9a8c7f881a8bce0ef9009b74dfd14fe7ed9243c1 Mon Sep 17 00:00:00 2001 From: Ralph Matthes Date: Tue, 14 Feb 2017 16:30:52 +0100 Subject: [PATCH 2/7] =?UTF-8?q?generalize=20construction=20of=20pointed=20?= =?UTF-8?q?distributive=20law=20=CE=B4=20from=20option=20to=20generalized?= =?UTF-8?q?=20option?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit all proofs simply still go through then, for compatibility with previous development, trivially instantiate to option --- .../SubstitutionSystems/SignatureExamples.v | 68 ++++++++++++------- 1 file changed, 43 insertions(+), 25 deletions(-) diff --git a/UniMath/SubstitutionSystems/SignatureExamples.v b/UniMath/SubstitutionSystems/SignatureExamples.v index ba760c8a7b..641ca990c4 100644 --- a/UniMath/SubstitutionSystems/SignatureExamples.v +++ b/UniMath/SubstitutionSystems/SignatureExamples.v @@ -247,26 +247,26 @@ Qed. End δ_mul. -(* Construct the δ when G = option *) -Section option_sig. +(** Construct the δ when G is generalized option *) +Section genoption_sig. -Variables (C : precategory) (hsC : has_homsets C) (TC : Terminal C) (CC : BinCoproducts C). +Variables (C : precategory) (hsC : has_homsets C) (A : C) (CC : BinCoproducts C). Local Notation "'Ptd'" := (precategory_Ptd C hsC). -Let opt := option_functor CC TC. +Let genopt := constcoprod_functor1 CC A. -Definition δ_option_mor (Ze : Ptd) (c : C) : C ⟦ BinCoproductObject C (CC TC (pr1 Ze c)), - pr1 Ze (BinCoproductObject C (CC TC c)) ⟧. +Definition δ_genoption_mor (Ze : Ptd) (c : C) : C ⟦ BinCoproductObject C (CC A (pr1 Ze c)), + pr1 Ze (BinCoproductObject C (CC A c)) ⟧. Proof. -apply (@BinCoproductArrow _ _ _ (CC TC (pr1 Ze c)) (pr1 Ze (BinCoproductObject C (CC TC c)))). -- apply (BinCoproductIn1 _ (CC TC c) ;; pr2 Ze (BinCoproductObject _ (CC TC c))). -- apply (# (pr1 Ze) (BinCoproductIn2 _ (CC TC c))). +apply (@BinCoproductArrow _ _ _ (CC A (pr1 Ze c)) (pr1 Ze (BinCoproductObject C (CC A c)))). +- apply (BinCoproductIn1 _ (CC A c) ;; pr2 Ze (BinCoproductObject _ (CC A c))). +- apply (# (pr1 Ze) (BinCoproductIn2 _ (CC A c))). Defined. -Lemma is_nat_trans_δ_option_mor (Ze : Ptd) : - is_nat_trans (δ_source C hsC opt Ze : functor C C) (δ_target C hsC opt Ze : functor C C) - (δ_option_mor Ze). +Lemma is_nat_trans_δ_genoption_mor (Ze : Ptd) : + is_nat_trans (δ_source C hsC genopt Ze : functor C C) (δ_target C hsC genopt Ze : functor C C) + (δ_genoption_mor Ze). Proof. intros a b f; simpl. destruct Ze as [Z e]. @@ -293,14 +293,14 @@ apply pathsinv0, BinCoproductArrowUnique. now apply maponpaths, BinCoproductOfArrowsIn2. Qed. -Lemma is_nat_trans_δ_option_mor_nat_trans : is_nat_trans (δ_source_functor_data C hsC opt) - (δ_target_functor_data C hsC opt) - (λ Ze : Ptd, δ_option_mor Ze,, is_nat_trans_δ_option_mor Ze). +Lemma is_nat_trans_δ_genoption_mor_nat_trans : is_nat_trans (δ_source_functor_data C hsC genopt) + (δ_target_functor_data C hsC genopt) + (λ Ze : Ptd, δ_genoption_mor Ze,, is_nat_trans_δ_genoption_mor Ze). Proof. intros [Z e] [Z' e'] [α X]; simpl in *. apply (nat_trans_eq hsC); intro c; simpl. rewrite id_left, functor_id, id_right. -unfold BinCoproduct_of_functors_mor, BinCoproduct_of_functors_ob, δ_option_mor; simpl. +unfold BinCoproduct_of_functors_mor, BinCoproduct_of_functors_ob, δ_genoption_mor; simpl. rewrite precompWithBinCoproductArrow. apply pathsinv0, BinCoproductArrowUnique. - rewrite id_left, assoc. @@ -314,29 +314,29 @@ apply pathsinv0, BinCoproductArrowUnique. now apply nat_trans_ax. Qed. -Definition δ_option : δ_source C hsC opt ⟶ δ_target C hsC opt. +Definition δ_genoption : δ_source C hsC genopt ⟶ δ_target C hsC genopt. Proof. mkpair. - intro Ze. - apply (tpair _ (δ_option_mor Ze) (is_nat_trans_δ_option_mor Ze)). -- apply is_nat_trans_δ_option_mor_nat_trans. + apply (tpair _ (δ_genoption_mor Ze) (is_nat_trans_δ_genoption_mor Ze)). +- apply is_nat_trans_δ_genoption_mor_nat_trans. Defined. -Lemma δ_law1_option : δ_law1 C hsC opt δ_option. +Lemma δ_law1_genoption : δ_law1 C hsC genopt δ_genoption. Proof. apply (nat_trans_eq hsC); intro c; simpl. -unfold δ_option_mor, BinCoproduct_of_functors_ob; simpl. +unfold δ_genoption_mor, BinCoproduct_of_functors_ob; simpl. rewrite id_right. apply pathsinv0, BinCoproduct_endo_is_identity. - apply BinCoproductIn1Commutes. - apply BinCoproductIn2Commutes. Qed. -Lemma δ_law2_option : δ_law2 C hsC opt δ_option. +Lemma δ_law2_genoption : δ_law2 C hsC genopt δ_genoption. Proof. intros [Z e] [Z' e']. apply (nat_trans_eq hsC); intro c; simpl. -unfold δ_option_mor, BinCoproduct_of_functors_ob; simpl. +unfold δ_genoption_mor, BinCoproduct_of_functors_ob; simpl. rewrite !id_left, id_right. apply pathsinv0, BinCoproductArrowUnique. - rewrite assoc. @@ -358,8 +358,26 @@ apply pathsinv0, BinCoproductArrowUnique. now apply maponpaths, BinCoproductIn2Commutes. Qed. -Definition precomp_option_Signature : Signature C hsC := - θ_from_δ_Signature _ hsC opt δ_option δ_law1_option δ_law2_option. +Definition precomp_genoption_Signature : Signature C hsC := + θ_from_δ_Signature _ hsC genopt δ_genoption δ_law1_genoption δ_law2_genoption. + + +End genoption_sig. + + +(** trivially instantiate previous section to option functor *) +Section option_sig. + + Variables (C : precategory) (hsC : has_homsets C) (TC : Terminal C) (CC : BinCoproducts C). + Let opt := option_functor CC TC. + Definition δ_option: δ_source C hsC opt ⟶ δ_target C hsC opt := + δ_genoption C hsC TC CC. + + Definition δ_law1_option := δ_law1_genoption C hsC TC CC. + Definition δ_law2_option := δ_law2_genoption C hsC TC CC. + + Definition precomp_option_Signature : Signature C hsC := + precomp_genoption_Signature C hsC TC CC. End option_sig. From 65a14daeabcee16e7e30661f2b1fd312641af20e Mon Sep 17 00:00:00 2001 From: Ralph Matthes Date: Tue, 14 Feb 2017 17:43:42 +0100 Subject: [PATCH 3/7] option functor in multisorted setting from general principles this uses the generalized option functor with a constant that is not a terminal object --- UniMath/SubstitutionSystems/MultiSorted.v | 49 ++++++++++------------- 1 file changed, 21 insertions(+), 28 deletions(-) diff --git a/UniMath/SubstitutionSystems/MultiSorted.v b/UniMath/SubstitutionSystems/MultiSorted.v index 8647262c55..cf474b24cc 100644 --- a/UniMath/SubstitutionSystems/MultiSorted.v +++ b/UniMath/SubstitutionSystems/MultiSorted.v @@ -69,6 +69,19 @@ exists (SET / sort). now apply has_homsets_slice_precat. Defined. +(* will not be needed: *) +Local Definition BinCoproducts_SET_over_sort: BinCoproducts SET_over_sort. +Proof. +apply BinCoproducts_slice_precat. +exact BinCoproductsHSET. +Defined. + +Local Definition BinCoproducts_SET_div_sort: BinCoproducts (SET / sort). +Proof. +apply BinCoproducts_slice_precat. +exact BinCoproductsHSET. +Defined. + Let post_comp := post_composition_functor (SET / sort) _ _ (homset_property SET_over_sort) has_homsets_HSET. @@ -109,44 +122,24 @@ mkpair. apply subtypeEquality; try (intro x; apply has_homsets_HSET)). Defined. -Local Definition option_fun : sort -> SET / sort -> SET / sort. +Definition sorted_variable (s: sort) : SET / sort. Proof. - simpl; intros s Xf. mkpair. + mkpair. - - exact (pr1 (pr1 Xf) ⨿ unit). - - apply isasetcoprod; [apply setproperty| apply isasetunit]. - + exact (sumofmaps (pr2 Xf) (termfun s)). + - exact unit. + - apply isasetunit. + + intros _. exact s. Defined. -Local Definition option_functor_data (s : sort) : functor_data (SET / sort) (SET / sort). -Proof. -exists (option_fun s). -intros X Y f. -mkpair. -- intros F. - induction F as [t|t]; [apply (ii1 (pr1 f t)) | apply (ii2 t)]. -- abstract (apply funextsec; intros [t|t]; trivial; apply (toforallpaths _ _ _ (pr2 f) t)). -Defined. - -Local Lemma is_functor_option_functor (s : sort) : is_functor (option_functor_data s). -Proof. -split; simpl. -+ intros X; apply (eq_mor_slicecat has_homsets_HSET), funextsec; intros t. - now induction t. -+ intros X Y Z f g; apply (eq_mor_slicecat has_homsets_HSET), funextsec; intros t. - now induction t. -Qed. +Definition sorted_option_functor (s : sort) : functor (SET / sort) (SET / sort) := + constcoprod_functor1 BinCoproducts_SET_div_sort (sorted_variable s). -Local Definition option_functor (s : sort) : functor (SET / sort) (SET / sort) := - tpair _ _ (is_functor_option_functor s). - -(** option_functor for lists (also called option in the note) *) +(** sorted option functor for lists (also called option in the note) *) Local Definition option_list (xs : list sort) : functor (SET / sort) (SET / sort). Proof. use (foldr _ _ xs). + intros s F. - apply (functor_composite (option_functor s) F). + apply (functor_composite (sorted_option_functor s) F). + apply functor_identity. Defined. From 3940dd9fae13c0004276b3b95d2f45d3ef7e62c0 Mon Sep 17 00:00:00 2001 From: Ralph Matthes Date: Tue, 14 Feb 2017 18:00:27 +0100 Subject: [PATCH 4/7] sorted_variable had been already defined before under a different name original definition moved up --- UniMath/SubstitutionSystems/MultiSorted.v | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/UniMath/SubstitutionSystems/MultiSorted.v b/UniMath/SubstitutionSystems/MultiSorted.v index cf474b24cc..7fa83385ba 100644 --- a/UniMath/SubstitutionSystems/MultiSorted.v +++ b/UniMath/SubstitutionSystems/MultiSorted.v @@ -122,17 +122,15 @@ mkpair. apply subtypeEquality; try (intro x; apply has_homsets_HSET)). Defined. -Definition sorted_variable (s: sort) : SET / sort. +(** The object (1,λ _,s) in SET/sort that can be seen as a sorted variable *) +Local Definition constHSET_slice (s : sort) : SET / sort. Proof. - mkpair. - + mkpair. - - exact unit. - - apply isasetunit. - + intros _. exact s. +exists (TerminalObject TerminalHSET); simpl. +apply (λ x, s). Defined. Definition sorted_option_functor (s : sort) : functor (SET / sort) (SET / sort) := - constcoprod_functor1 BinCoproducts_SET_div_sort (sorted_variable s). + constcoprod_functor1 BinCoproducts_SET_div_sort (constHSET_slice s). (** sorted option functor for lists (also called option in the note) *) Local Definition option_list (xs : list sort) : functor (SET / sort) (SET / sort). @@ -193,13 +191,6 @@ End functor. (** * Proof that the functor obtained from a multisorted signature is omega-cocontinuous *) Section omega_cocont. -(** The object (1,λ _,s) in SET/sort *) -Local Definition constHSET_slice (s : sort) : SET / sort. -Proof. -exists (TerminalObject TerminalHSET); simpl. -apply (λ x, s). -Defined. - (** 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 := functor_composite From d47ec2fb3b04f4dee7ab04c2537c0825f962561a Mon Sep 17 00:00:00 2001 From: Ralph Matthes Date: Tue, 14 Feb 2017 18:23:13 +0100 Subject: [PATCH 5/7] cleaning the development: more uniform proofs with HSET properties --- UniMath/CategoryTheory/category_hset_structures.v | 6 ++++++ UniMath/SubstitutionSystems/MultiSorted.v | 15 +-------------- 2 files changed, 7 insertions(+), 14 deletions(-) diff --git a/UniMath/CategoryTheory/category_hset_structures.v b/UniMath/CategoryTheory/category_hset_structures.v index f327e7a45f..9e2d1eb61d 100644 --- a/UniMath/CategoryTheory/category_hset_structures.v +++ b/UniMath/CategoryTheory/category_hset_structures.v @@ -732,6 +732,12 @@ Proof. now apply BinProducts_slice_precat, PullbacksHSET. Defined. +Lemma BinCoproducts_HSET_slice X : BinCoproducts (HSET / X). +Proof. +now apply BinCoproducts_slice_precat, BinCoproductsHSET. +Defined. + + (** Direct proof that HSET/X has exponentials using explicit formula in example 2.2 of: https://ncatlab.org/nlab/show/locally+cartesian+closed+category#in_category_theory diff --git a/UniMath/SubstitutionSystems/MultiSorted.v b/UniMath/SubstitutionSystems/MultiSorted.v index 7fa83385ba..31c08b51ce 100644 --- a/UniMath/SubstitutionSystems/MultiSorted.v +++ b/UniMath/SubstitutionSystems/MultiSorted.v @@ -69,19 +69,6 @@ exists (SET / sort). now apply has_homsets_slice_precat. Defined. -(* will not be needed: *) -Local Definition BinCoproducts_SET_over_sort: BinCoproducts SET_over_sort. -Proof. -apply BinCoproducts_slice_precat. -exact BinCoproductsHSET. -Defined. - -Local Definition BinCoproducts_SET_div_sort: BinCoproducts (SET / sort). -Proof. -apply BinCoproducts_slice_precat. -exact BinCoproductsHSET. -Defined. - Let post_comp := post_composition_functor (SET / sort) _ _ (homset_property SET_over_sort) has_homsets_HSET. @@ -130,7 +117,7 @@ apply (λ x, s). Defined. Definition sorted_option_functor (s : sort) : functor (SET / sort) (SET / sort) := - constcoprod_functor1 BinCoproducts_SET_div_sort (constHSET_slice s). + constcoprod_functor1 (BinCoproducts_HSET_slice sort) (constHSET_slice s). (** sorted option functor for lists (also called option in the note) *) Local Definition option_list (xs : list sort) : functor (SET / sort) (SET / sort). From 5cd40676714cddd71dbc6cfcbf7fa6315ee464ba Mon Sep 17 00:00:00 2001 From: Ralph Matthes Date: Tue, 14 Feb 2017 20:15:46 +0100 Subject: [PATCH 6/7] explanatory comments for three functor definitions --- UniMath/SubstitutionSystems/MultiSorted.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/UniMath/SubstitutionSystems/MultiSorted.v b/UniMath/SubstitutionSystems/MultiSorted.v index 31c08b51ce..dcc8263a4d 100644 --- a/UniMath/SubstitutionSystems/MultiSorted.v +++ b/UniMath/SubstitutionSystems/MultiSorted.v @@ -83,6 +83,7 @@ Definition arity (M : MultiSortedSig) : ops M → list (list sort × sort) × so (** * Construction of an endofunctor on [SET/sort,SET/sort] from a multisorted signature *) Section functor. +(** identify the set of variables of a given sort, i.e,. project a typing environment to that set *) Local Definition proj_fun (s : sort) : SET / sort -> SET := λ p, hfiber_hSet (pr2 p) s. @@ -98,7 +99,7 @@ mkpair. intros x; apply setproperty). Defined. -(** The left adjoint to the proj_functor *) +(** build constant typing environments, yields a left adjoint to the proj_functor *) Local Definition hat_functor (t : sort) : functor SET (SET / sort). Proof. mkpair. @@ -116,6 +117,7 @@ exists (TerminalObject TerminalHSET); simpl. apply (λ x, s). Defined. +(** add a sorted variable to a typing environment *) Definition sorted_option_functor (s : sort) : functor (SET / sort) (SET / sort) := constcoprod_functor1 (BinCoproducts_HSET_slice sort) (constHSET_slice s). From ebaee30db20d1c5e17f447e6fcf4bd884e84a3f9 Mon Sep 17 00:00:00 2001 From: Ralph Matthes Date: Tue, 14 Feb 2017 20:21:51 +0100 Subject: [PATCH 7/7] one typo in comment --- UniMath/SubstitutionSystems/MultiSorted.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/UniMath/SubstitutionSystems/MultiSorted.v b/UniMath/SubstitutionSystems/MultiSorted.v index dcc8263a4d..58fe8c8512 100644 --- a/UniMath/SubstitutionSystems/MultiSorted.v +++ b/UniMath/SubstitutionSystems/MultiSorted.v @@ -83,7 +83,7 @@ Definition arity (M : MultiSortedSig) : ops M → list (list sort × sort) × so (** * Construction of an endofunctor on [SET/sort,SET/sort] from a multisorted signature *) Section functor. -(** identify the set of variables of a given sort, i.e,. project a typing environment to that set *) +(** identify the set of variables of a given sort, i.e., project a typing environment to that set *) Local Definition proj_fun (s : sort) : SET / sort -> SET := λ p, hfiber_hSet (pr2 p) s.