More general option functor

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

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.
 

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

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.