Brought documentation of precats vs. cats up to date with code (wherever I found discrepancies)

Author: peterlefanulumsdaine

TypeTheory/ALV1/CwF_SplitTypeCat_Defs.v

@@ -8,17 +8,17 @@
 
 In this file, we give the definitions of _split type-categories_ (originally due to Cartmell, here following a version given by Pitts) and _categories with families_ (originally due to Dybjer, here following a formulation given by Fiore).
 
-To facilitate comparing them afterwards, we split up their definitions in a slightly unusual way, starting with the part they share.  The key definitions of this file are therefore (all over a fixed base (pre)category [C]):  
+To facilitate comparing them afterwards, we split up their definitions in a slightly unusual way, starting with the part they share.  The key definitions of this file are therefore (all over a fixed base category [C]):
 
 - _object-extension structures_, [obj_ext_structure], the common core of CwF’s and split type-categories;
 - (_functional) term structures_, [term_fun_structure], the rest of the structure of a CwF on [C];
-- _cwf-structures_, [cwf_structure], the full structure of a CwF on a precategory [C]; 
+- _cwf-structures_, [cwf_structure], the full structure of a CwF on a category [C];
 - _CwF’s_, [cwf]; 
 - _q-morphism structures_, [qq_morphism_structure], for rest of the structure of a split type-category on [C];
 - _split type-cat structures_, [split_typecat_structure], the full structure of a split type-category on [C].
 - _split type-categories_, [split_typecat].
 
-NB: we follow the convention that _category_ does not include an assumption of saturation/univalence, i.e. means what is sometimes called _precategory_.
+NB: we follow UniMath’s convention that _category_ does not assume saturation/univalence, i.e. means what is sometimes called _precategory_ in the literature.
 *)
 
 
@@ -526,9 +526,7 @@ End Families_Structures.
 
 Section qq_Morphism_Structures.
 
-(* NOTE: most of this section does not require the [homset_property] for [C]. If the few lemmas that do require it were moved out of the section, e.g. [isaprop_qq_morphism_axioms], then would could take [C] as just a [precategory] here. Perhaps worth doing so?
-
-(Another alternative would be adding an extra argument of type [has_homsets C] to [isaprop_qq_morphism_axioms], but that’s less convenient for later use than just having [C] be a [category] in those lemmas.) *)
+(* NOTE: most of this section does not require the [homset_property] for [C]. If the few lemmas that do require it were moved out of the section, e.g. [isaprop_qq_morphism_axioms], then would could take [C] as just a [precategory] here. Perhaps worth doing so? Would mainly be relevant if we wanted to generalise to bicategories. *)
 
 Context {C : category} {X : obj_ext_structure C}.
 

TypeTheory/ALV1/TypeCat.v

@@ -5,7 +5,7 @@
 
 Contents:
 
-  - Definition of type-categories and split type-categories
+  - Definition of type-(pre)categories and split type-categories
   - A few convenience lemmas
 *)
 
@@ -34,13 +34,12 @@ However, that definition includes two _strictness conditions_;
 we follow van den Berg and Garner, _Topological and simplicial models_, Def 2.2.1 #(<a href="http://arxiv.org/abs/1007.4638">arXiv</a>)# 
 in separating these out from the rest of the definition.
 
- An element of [type_precat], as we define it below, is thus exactly a type-category according 
-to the definition of van den Berg and Garner; and an element of [split_type_precat] is a split type-category 
-according to van den Berg and Garner, or a plain type-category in the sense of Pitts 
-(modulo, in either case, the question of equality on objects of the category).
- 
+ An element of [typecat], as we define it below, is thus exactly a type-category according 
+to the definition of van den Berg and Garner (except with an underlying _precategory_, i.e. hom-types not assumed sets); and an element of [split_typecat] is a split type-category 
+according to van den Berg and Garner, or a plain type-category in the sense of Pitts.
+
   In order to avoid the nested sigma-types getting too deep, 
-we split up the structure into two stages: [type_precat_structure1] and [type_precat_structure2]. *)
+we split up the structure into two stages: [typecat_structure1] and [typecat_structure2]. *)
 
 (** * A "preview" of the definition *)
 
@@ -174,8 +173,8 @@ Definition is_type_saturated_typecat {CC : precategory} (C : typecat_structure C
 
 (** * Splitness *)
 
-(** A type-precategory [C] is _split_ if each collection of types [C Γ] is a set, reindexing is strictly functorial, and the [q] maps satisfy the evident functoriality axioms *) 
-Definition is_split_typecat {CC : precategory} (C : typecat_structure CC)
+(** A type-precategory [C] is _split_ if it is a category (i.e. has hom-sets); each collection of types [C Γ] is a set, reindexing is strictly functorial; and the [q] maps satisfy the evident functoriality axioms *) 
+Definition is_split_typecat {CC : category} (C : typecat_structure CC)
   := (∏ Γ:CC, isaset (C Γ))
      × (∑ (reind_id : ∏ Γ (A : C Γ), A {{identity Γ}} = A),
          ∏ Γ (A : C Γ), q_typecat A (identity Γ)
@@ -210,14 +209,14 @@ Definition split_typecat := ∑ (C : typecat), (is_split_typecat C).
 Coercion typecat_of_split_typecat (C : split_typecat) := pr1 C.
 Coercion split_typecat_is_split (C : split_typecat) := pr2 C.
 
-Definition split_typecat_structure (CC : precategory) : UU
+Definition split_typecat_structure (CC : category) : UU
   := ∑ C : typecat_structure CC, is_split_typecat C.
 
-Coercion typecat_from_split (CC : precategory) (C : split_typecat_structure CC)
+Coercion typecat_from_split (CC : category) (C : split_typecat_structure CC)
   : typecat_structure _
   := pr1 C.
 
-Coercion is_split_from_split_typecat (CC : precategory) (C : split_typecat_structure CC)
+Coercion is_split_from_split_typecat (CC : category) (C : split_typecat_structure CC)
   : is_split_typecat C
   := pr2 C.
 

TypeTheory/Categories/ess_alg_categories.v

@@ -1,7 +1,7 @@
 
-(** (Pre)-categories in essentially algebraic style *)
+(** Categories in essentially algebraic style *)
 
-(** Such a (pre-)category is given by
+(** Such a category is given by
     - a type (set) of objects
     - a type (set) of morphisms
     - source and target maps
@@ -208,4 +208,4 @@ Proof.
   exact (pr2 (pr2 (pr1 (pr2 (pr2 C))))).
 Qed.
 
-End access_functions.
+End access_functions.

TypeTheory/OtherDefs/CwF_1.v

@@ -5,7 +5,7 @@
 
   Contents:
 
-    - Definition of a precategory with families
+    - Definition of a category with families
     - Proof that reindexing forms a pullback
 
   The definition is based on Pitts, *Nominal Presentations of the Cubical Sets
@@ -36,8 +36,8 @@ Reserved Notation "'π' A" (at level 20).
 Reserved Notation "'ν' A" (at level 15).
 Reserved Notation "γ ♯ a" (at level 25).
 (*
-Record precwf_record : Type := {
-  C : precategory ;
+Record cwf_record : Type := {
+  C : category ;
   Ty : functor C HSET     where "C ⟨ Γ ⟩" := (Ty Γ) ;
   term : ∏ Γ : C, pr1hSet (Ty Γ) → UU     where "C ⟨ Γ ⊢ A ⟩" := (term Γ A) ;
 (*  rtype : ∏ {Γ Γ' : C} (A : pr1hSet (Ty Γ)) (γ : Γ' --> Γ), pr1hSetC⟨Γ'⟩ where "A [[ γ ]]" := (rtype A γ) ; *)
@@ -61,12 +61,12 @@ Record precwf_record : Type := {
   gen_element : ∏ Γ (A : C⟨Γ⟩), C⟨Γ∙A ⊢ A[[π _ ]]⟩ where "'ν' A" := (gen_element _ A) ;
   pairing : ∏ Γ (A : C⟨Γ⟩) Γ' (γ : Γ' --> Γ)(a : C⟨Γ'⊢ A[[γ]]⟩), Γ' --> Γ∙A 
      where "γ ♯ a" := (pairing _ _ _  γ a) ;
-  pre_cwf_law_1 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩), 
+  cwf_law_1 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩), 
           (γ ♯ a) ;; (π _) 
           = 
           γ ;
-  pre_cwf_law_2 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩),
-          transportf (λ ι, C⟨Γ'⊢ A [[ι]]⟩) (pre_cwf_law_1 Γ A Γ' γ a)
+  cwf_law_2 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩),
+          transportf (λ ι, C⟨Γ'⊢ A [[ι]]⟩) (cwf_law_1 Γ A Γ' γ a)
              (transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp (π _ )(γ ♯ a) _ )
                 ((ν A) ⟦γ ♯ a⟧))
           = 
@@ -77,11 +77,15 @@ End Record_Preview.
 
 
 (** * Type and terms of a [CwF] *)
+
+(* Note: in the end, we define not pre-cwfs but cwfs, assuming an underlying _category_ with homsets.  But for the “data” stages of the definition, we just take an underlying precategory. *)
+
 (** 
- A [tt_precategory] comes with a types, written [C⟨Γ⟩], 
+ A [cwf] comes with types, written [C⟨Γ⟩], 
    and terms [C⟨Γ ⊢ A⟩] 
 *)
 
+
 Definition tt_structure (C : precategory) :=
   ∑ f : functor C^op HSET, ∏ c : C, pr1hSet (f c) → UU.
 
@@ -281,9 +285,9 @@ Definition cwf_laws {CC : category} (C : tt_reindx_type_struct CC)
        (comp_laws_1_2 T × comp_law_3 T × comp_law_4 T)) ×
     (∏ Γ (A : C⟨Γ⟩), isaset (C⟨Γ⊢ A⟩)). 
 
-(** * Definition of precategory with families *)
-(** A precategory with families [pre_cwf] is 
-  - a precategory
+(** * Definition of category with families *)
+(** A category with families [cwf] is 
+  - a category
   - with type-and-term structure 
   - with reindexing 
   - with comprehension structure
@@ -403,7 +407,7 @@ Section CwF_lemmas.
 Generalizable Variable CC.
 Context `{C : cwf_struct CC}.
 
-Lemma map_to_comp_as_pair_precwf {Γ} {A : C⟨Γ⟩} {Γ'} (f : Γ' --> Γ∙A)
+Lemma map_to_comp_as_pair_cwf {Γ} {A : C⟨Γ⟩} {Γ'} (f : Γ' --> Γ∙A)
   :   (f ;; π A) ♯ (transportb _ (reindx_type_comp _ _ _) ((gen_elem A)⟦f⟧))
       = 
       f.
@@ -503,8 +507,8 @@ Proof.
   apply idpath.
 Qed.
 
-(* TODO: consider giving this instead of current [pre_cwf_law_2] ? *)
-Definition pre_cwf_law_2' Γ (A : C ⟨ Γ ⟩) Γ' (γ : Γ' --> Γ) (a : C ⟨ Γ' ⊢ A[[γ]] ⟩)
+(* TODO: consider giving this instead of current [cwf_law_2] ? *)
+Definition cwf_law_2' Γ (A : C ⟨ Γ ⟩) Γ' (γ : Γ' --> Γ) (a : C ⟨ Γ' ⊢ A[[γ]] ⟩)
   : (ν A) ⟦γ ♯ a⟧
   = transportf _ (reindx_type_comp _ _ _)
       (transportb _ (maponpaths (fun g => A[[g]]) (cwf_law_1 _ _ _ _ _ _))
@@ -530,7 +534,7 @@ Proof.
   apply id_right.
 Defined.
 
-Definition q_precwf {Γ} (A : C ⟨ Γ ⟩ ) {Γ'} (f : Γ' --> Γ)
+Definition q_cwf {Γ} (A : C ⟨ Γ ⟩ ) {Γ'} (f : Γ' --> Γ)
   : (comp_obj  Γ' (A[[f]])) --> (Γ ∙ A).
 Proof.
   set (T:= @pairing _ C).
@@ -539,28 +543,28 @@ Proof.
   apply gen_elem.
 Defined.
 
-Definition dpr_q_precwf 
+Definition dpr_q_cwf 
   {Γ} (A : C ⟨ Γ ⟩)
   {Γ'} (f : Γ' --> Γ)
-: (q_precwf A f) ;; (π A) = (π (A[[f]])) ;; f.
+: (q_cwf A f) ;; (π A) = (π (A[[f]])) ;; f.
 Proof.
-  unfold q_precwf.
+  unfold q_cwf.
   apply cwf_law_1.
 Qed.
 
 
 Lemma rterm_univ {Γ} {A : C ⟨ Γ ⟩} {Γ'} (f : Γ' --> Γ)
   : ν (A[[f]])
    = transportf _ (reindx_type_comp _ _ _)
-       (transportf _ (maponpaths (fun g => A[[g]]) (dpr_q_precwf A f))
+       (transportf _ (maponpaths (fun g => A[[g]]) (dpr_q_cwf A f))
          (transportb _ (reindx_type_comp _ _ _)
-            ((ν A)⟦q_precwf A f⟧))).
+            ((ν A)⟦q_cwf A f⟧))).
 Proof.
   sym.
   rew_trans_@.
   etrans.
   - apply maponpaths.
-    apply pre_cwf_law_2'.
+    apply cwf_law_2'.
   - rew_trans_@.
     apply term_typeeq_transport_lemma_2.
     apply idpath.
@@ -576,7 +580,7 @@ We split this up into several lemmas:
 
 *)
 
-Definition dpr_q_pbpairing_precwf_aux
+Definition dpr_q_pbpairing_cwf_aux
   {Γ} (A : C ⟨ Γ ⟩)
   {Γ'} (f : Γ' --> Γ)
   {X} (h : X --> Γ ∙ A) (k : X --> Γ') (H : h ;; π A = k ;; f)
@@ -590,16 +594,16 @@ Definition dpr_q_pbpairing_commutes
   {Γ} (A : C ⟨ Γ ⟩)
   {Γ'} (f : Γ' --> Γ)
   {X} (h : X --> Γ ∙ A) (k : X --> Γ') (H : h ;; π A = k ;; f)
-  (hk := @pairing _ C Γ' (A[[f]]) X k (dpr_q_pbpairing_precwf_aux A f h k H))
-: (hk ;; q_precwf A f = h) × (hk ;; π (A[[f]]) = k).
+  (hk := @pairing _ C Γ' (A[[f]]) X k (dpr_q_pbpairing_cwf_aux A f h k H))
+: (hk ;; q_cwf A f = h) × (hk ;; π (A[[f]]) = k).
 Proof.
   split. 2: { apply cwf_law_1. }
-  unfold q_precwf.
+  unfold q_cwf.
   etrans.
-  2: { apply map_to_comp_as_pair_precwf. }
+  2: { apply map_to_comp_as_pair_cwf. }
   etrans.
     apply cwf_law_3.
-  assert ((k ♯ (dpr_q_pbpairing_precwf_aux A f h k H)) ;; (π (A [[f]]) ;; f) 
+  assert ((k ♯ (dpr_q_pbpairing_cwf_aux A f h k H)) ;; (π (A [[f]]) ;; f) 
           = h ;; π A) as e1.
     eapply pathscomp0. apply assoc.
     refine (_ @ !H).
@@ -610,38 +614,38 @@ Proof.
   eapply pathscomp0. apply transport_f_f.
   eapply pathscomp0. apply maponpaths. refine (! rterm_typeeq _ _ _).
   eapply pathscomp0. apply transport_f_f.
-  eapply pathscomp0. apply maponpaths, pre_cwf_law_2'.
+  eapply pathscomp0. apply maponpaths, cwf_law_2'.
   rew_trans_@.
   eapply pathscomp0. apply maponpaths, transportf_rtype_mapeq.
   repeat (eapply pathscomp0; [ apply transport_f_f | ]).
   refine (maponpaths (fun e => transportf _ e _) _).
   apply cwf_types_isaset.
 Qed.
 
-Definition dpr_q_pbpairing_precwf
+Definition dpr_q_pbpairing_cwf
   {Γ} (A : C ⟨ Γ ⟩)
   {Γ'} (f : Γ' --> Γ)
   {X} (h : X --> Γ ∙ A) (k : X --> Γ') (H : h ;; π A = k ;; f)
 : ∑ (hk : X --> Γ' ∙ (A[[f]])),
-    ( hk ;; q_precwf A f = h
+    ( hk ;; q_cwf A f = h
     × hk ;; π (A[[f]]) = k).
 Proof.
-  exists (@pairing _ C Γ' (A[[f]]) X k (dpr_q_pbpairing_precwf_aux A f h k H)).
+  exists (@pairing _ C Γ' (A[[f]]) X k (dpr_q_pbpairing_cwf_aux A f h k H)).
   apply dpr_q_pbpairing_commutes.
 Defined.
 
 
-Definition dpr_q_pbpairing_precwf_mapunique
+Definition dpr_q_pbpairing_cwf_mapunique
   {Γ} (A : C⟨Γ⟩)
   {Γ'} (f : Γ' --> Γ)
   {X} {h : X --> Γ ∙ A} {k : X --> Γ'} (H : h ;; π A = k ;; f)
   (hk : X --> Γ' ∙ (A [[f]]))
-  (e2 : hk ;; q_precwf A f = h)
+  (e2 : hk ;; q_cwf A f = h)
   (e1 : hk ;; π (A[[f]]) = k)
-: hk = pr1 (dpr_q_pbpairing_precwf A f h k H).
+: hk = pr1 (dpr_q_pbpairing_cwf A f h k H).
 Proof.
   eapply pathscomp0.
-    eapply pathsinv0. apply map_to_comp_as_pair_precwf.
+    eapply pathsinv0. apply map_to_comp_as_pair_cwf.
   eapply pathscomp0.
     apply (pairing_mapeq _ _ e1 _).
   simpl. apply maponpaths.
@@ -673,29 +677,29 @@ Proof.
   apply idpath.
 Qed.
 
-Definition dpr_q_pbpairing_precwf_unique
+Definition dpr_q_pbpairing_cwf_unique
   {Γ} (A : C⟨Γ⟩)
   {Γ'} (f : Γ' --> Γ)
   {X} (h : X --> Γ ∙ A) (k : X --> Γ') (H : h ;; π A = k ;; f)
   (t : ∑ hk : X --> Γ' ∙ (A [[f]]),
-       (hk ;; q_precwf A f = h) × (hk ;; π (A[[f]]) = k))
-: t = dpr_q_pbpairing_precwf A f h k H.
+       (hk ;; q_cwf A f = h) × (hk ;; π (A[[f]]) = k))
+: t = dpr_q_pbpairing_cwf A f h k H.
 Proof.
   destruct t as [hk [e2 e1] ]. 
   unshelve refine (@total2_paths_f _ _ (tpair _ hk (tpair _ e2 e1)) _ 
-    (dpr_q_pbpairing_precwf_mapunique A f H hk e2 e1) _).
+    (dpr_q_pbpairing_cwf_mapunique A f H hk e2 e1) _).
   unshelve refine (total2_paths_f _ _); apply homset_property.
 Qed.
 
 Lemma is_pullback_reindx_cwf : ∏ (Γ : CC) (A : C⟨Γ⟩) (Γ' : CC) 
    (f : Γ' --> Γ),
-   isPullback (dpr_q_precwf A f).
+   isPullback (dpr_q_cwf A f).
 Proof.
   intros.
   apply make_isPullback; try assumption.
   intros e h k H.
-  exists (dpr_q_pbpairing_precwf _ _ h k H).
-  apply dpr_q_pbpairing_precwf_unique.
+  exists (dpr_q_pbpairing_cwf _ _ h k H).
+  apply dpr_q_pbpairing_cwf_unique.
 Defined.
 
 End CwF_lemmas.