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/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. diff --git a/UniMath/SubstitutionSystems/MultiSorted.v b/UniMath/SubstitutionSystems/MultiSorted.v index 8647262c55..58fe8c8512 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. @@ -109,44 +110,23 @@ mkpair. apply subtypeEquality; try (intro x; apply has_homsets_HSET)). Defined. -Local Definition option_fun : sort -> SET / 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)). -Defined. - -Local Definition option_functor_data (s : sort) : functor_data (SET / 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. -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)). +exists (TerminalObject TerminalHSET); simpl. +apply (λ x, s). 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. +(** 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). -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. @@ -200,13 +180,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 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.