You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: TypeTheory/ALV1/CwF_SplitTypeCat_Defs.v
+4-6Lines changed: 4 additions & 6 deletions
Original file line number
Diff line number
Diff line change
@@ -8,17 +8,17 @@
8
8
9
9
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).
10
10
11
-
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]):
11
+
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]):
12
12
13
13
- _object-extension structures_, [obj_ext_structure], the common core of CwF’s and split type-categories;
14
14
- (_functional) term structures_, [term_fun_structure], the rest of the structure of a CwF on [C];
15
-
- _cwf-structures_, [cwf_structure], the full structure of a CwF on a precategory [C];
15
+
- _cwf-structures_, [cwf_structure], the full structure of a CwF on a category [C];
16
16
- _CwF’s_, [cwf];
17
17
- _q-morphism structures_, [qq_morphism_structure], for rest of the structure of a split type-category on [C];
18
18
- _split type-cat structures_, [split_typecat_structure], the full structure of a split type-category on [C].
19
19
- _split type-categories_, [split_typecat].
20
20
21
-
NB: we follow the convention that _category_ does not include an assumption of saturation/univalence, i.e. means what is sometimes called _precategory_.
21
+
NB: we follow UniMath’s convention that _category_ does not assume saturation/univalence, i.e. means what is sometimes called _precategory_ in the literature.
22
22
*)
23
23
24
24
@@ -526,9 +526,7 @@ End Families_Structures.
526
526
527
527
Section qq_Morphism_Structures.
528
528
529
-
(* 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?
530
-
531
-
(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.) *)
529
+
(* 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. *)
Copy file name to clipboardExpand all lines: TypeTheory/ALV1/TypeCat.v
+15-17Lines changed: 15 additions & 17 deletions
Original file line number
Diff line number
Diff line change
@@ -5,7 +5,7 @@
5
5
6
6
Contents:
7
7
8
-
- Definition of type-categories and split type-categories
8
+
- Definition of type-(pre)categories and split type-categories
9
9
- A few convenience lemmas
10
10
*)
11
11
@@ -34,13 +34,12 @@ However, that definition includes two _strictness conditions_;
34
34
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>)#
35
35
in separating these out from the rest of the definition.
36
36
37
-
An element of [type_precat], as we define it below, is thus exactly a type-category according
38
-
to the definition of van den Berg and Garner; and an element of [split_type_precat] is a split type-category
39
-
according to van den Berg and Garner, or a plain type-category in the sense of Pitts
40
-
(modulo, in either case, the question of equality on objects of the category).
41
-
37
+
An element of [typecat], as we define it below, is thus exactly a type-category according
38
+
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
39
+
according to van den Berg and Garner, or a plain type-category in the sense of Pitts.
40
+
42
41
In order to avoid the nested sigma-types getting too deep,
43
-
we split up the structure into two stages: [type_precat_structure1] and [type_precat_structure2]. *)
42
+
we split up the structure into two stages: [typecat_structure1] and [typecat_structure2]. *)
(** 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 *)
(** 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 *)
0 commit comments