Nonunital precategories (#864)

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>

src/category-theory.lagda.md

@@ -25,6 +25,7 @@ open import category-theory.category-of-maps-categories public
 open import category-theory.category-of-maps-from-small-to-large-categories public
 open import category-theory.commuting-squares-of-morphisms-in-large-precategories public
 open import category-theory.commuting-squares-of-morphisms-in-precategories public
+open import category-theory.composition-operations-on-binary-families-of-sets public
 open import category-theory.coproducts-in-precategories public
 open import category-theory.dependent-products-of-categories public
 open import category-theory.dependent-products-of-large-categories public
@@ -94,6 +95,7 @@ open import category-theory.natural-transformations-functors-precategories publi
 open import category-theory.natural-transformations-maps-categories public
 open import category-theory.natural-transformations-maps-from-small-to-large-precategories public
 open import category-theory.natural-transformations-maps-precategories public
+open import category-theory.nonunital-precategories public
 open import category-theory.one-object-precategories public
 open import category-theory.opposite-precategories public
 open import category-theory.precategories public

src/category-theory/augmented-simplex-category.lagda.md

@@ -7,6 +7,7 @@ module category-theory.augmented-simplex-category where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.composition-operations-on-binary-families-of-sets
 open import category-theory.precategories
 
 open import elementary-number-theory.inequality-standard-finite-types
@@ -80,12 +81,13 @@ associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s} =
     ( Fin-Poset r)
     ( Fin-Poset s)
 
-associative-composition-structure-augmented-simplex-Category :
-  associative-composition-structure-Set hom-set-augmented-simplex-Category
-pr1 associative-composition-structure-augmented-simplex-Category {n} {m} {r} =
+associative-composition-operation-augmented-simplex-Category :
+  associative-composition-operation-binary-family-Set
+    hom-set-augmented-simplex-Category
+pr1 associative-composition-operation-augmented-simplex-Category {n} {m} {r} =
   comp-hom-augmented-simplex-Category {n} {m} {r}
 pr2
-  associative-composition-structure-augmented-simplex-Category {n} {m} {r} {s} =
+  associative-composition-operation-augmented-simplex-Category {n} {m} {r} {s} =
   associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s}
 
 id-hom-augmented-simplex-Category :
@@ -112,24 +114,24 @@ right-unit-law-comp-hom-augmented-simplex-Category :
 right-unit-law-comp-hom-augmented-simplex-Category {n} {m} =
   right-unit-law-comp-hom-Poset (Fin-Poset n) (Fin-Poset m)
 
-is-unital-composition-structure-augmented-simplex-Category :
-  is-unital-composition-structure-Set
+is-unital-composition-operation-augmented-simplex-Category :
+  is-unital-composition-operation-binary-family-Set
     ( hom-set-augmented-simplex-Category)
-    ( associative-composition-structure-augmented-simplex-Category)
-pr1 is-unital-composition-structure-augmented-simplex-Category =
+    ( λ {n} {m} {r} → comp-hom-augmented-simplex-Category {n} {m} {r})
+pr1 is-unital-composition-operation-augmented-simplex-Category =
   id-hom-augmented-simplex-Category
-pr1 (pr2 is-unital-composition-structure-augmented-simplex-Category) {n} {m} =
+pr1 (pr2 is-unital-composition-operation-augmented-simplex-Category) {n} {m} =
   left-unit-law-comp-hom-augmented-simplex-Category {n} {m}
-pr2 (pr2 is-unital-composition-structure-augmented-simplex-Category) {n} {m} =
+pr2 (pr2 is-unital-composition-operation-augmented-simplex-Category) {n} {m} =
   right-unit-law-comp-hom-augmented-simplex-Category {n} {m}
 
 augmented-simplex-Precategory : Precategory lzero lzero
 pr1 augmented-simplex-Precategory = obj-augmented-simplex-Category
 pr1 (pr2 augmented-simplex-Precategory) = hom-set-augmented-simplex-Category
 pr1 (pr2 (pr2 augmented-simplex-Precategory)) =
-  associative-composition-structure-augmented-simplex-Category
+  associative-composition-operation-augmented-simplex-Category
 pr2 (pr2 (pr2 augmented-simplex-Precategory)) =
-  is-unital-composition-structure-augmented-simplex-Category
+  is-unital-composition-operation-augmented-simplex-Category
 ```
 
 ### The augmented simplex category

src/category-theory/categories.lagda.md

@@ -7,8 +7,11 @@ module category-theory.categories where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.composition-operations-on-binary-families-of-sets
 open import category-theory.isomorphisms-in-precategories
+open import category-theory.nonunital-precategories
 open import category-theory.precategories
+open import category-theory.preunivalent-categories
 
 open import foundation.1-types
 open import foundation.dependent-pair-types
@@ -33,7 +36,9 @@ them, by the J-rule. A precategory is a category if this function, called
 being a category is a [proposition](foundation-core.propositions.md) since
 `is-equiv` is a proposition.
 
-## Definition
+## Definitions
+
+### The predicate on precategories of being a category
 
 ```agda
 module _
@@ -51,9 +56,13 @@ module _
 
   is-category-Precategory : UU (l1 ⊔ l2)
   is-category-Precategory = type-Prop is-category-prop-Precategory
+```
+
+### The type of categories
 
+```agda
 Category : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-Category l1 l2 = Σ (Precategory l1 l2) is-category-Precategory
+Category l1 l2 = Σ (Precategory l1 l2) (is-category-Precategory)
 
 module _
   {l1 l2 : Level} (C : Category l1 l2)
@@ -90,10 +99,10 @@ module _
   associative-comp-hom-Category =
     associative-comp-hom-Precategory precategory-Category
 
-  associative-composition-structure-Category :
-    associative-composition-structure-Set hom-set-Category
-  associative-composition-structure-Category =
-    associative-composition-structure-Precategory precategory-Category
+  associative-composition-operation-Category :
+    associative-composition-operation-binary-family-Set hom-set-Category
+  associative-composition-operation-Category =
+    associative-composition-operation-Precategory precategory-Category
 
   id-hom-Category : {x : obj-Category} → hom-Category x x
   id-hom-Category = id-hom-Precategory precategory-Category
@@ -110,18 +119,43 @@ module _
   right-unit-law-comp-hom-Category =
     right-unit-law-comp-hom-Precategory precategory-Category
 
-  is-unital-composition-structure-Category :
-    is-unital-composition-structure-Set
+  is-unital-composition-operation-Category :
+    is-unital-composition-operation-binary-family-Set
       hom-set-Category
-      associative-composition-structure-Category
-  is-unital-composition-structure-Category =
-    is-unital-composition-structure-Precategory precategory-Category
+      comp-hom-Category
+  is-unital-composition-operation-Category =
+    is-unital-composition-operation-Precategory precategory-Category
 
   is-category-Category :
     is-category-Precategory precategory-Category
   is-category-Category = pr2 C
 ```
 
+### The underlying nonunital precategory of a category
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2)
+  where
+
+  nonunital-precategory-Category : Nonunital-Precategory l1 l2
+  nonunital-precategory-Category =
+    nonunital-precategory-Precategory (precategory-Category C)
+```
+
+### The underlying preunivalent category of a category
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2)
+  where
+
+  preunivalent-category-Category : Preunivalent-Category l1 l2
+  pr1 preunivalent-category-Category = precategory-Category C
+  pr2 preunivalent-category-Category x y =
+    is-emb-is-equiv (is-category-Category C x y)
+```
+
 ### Precomposition by a morphism
 
 ```agda
@@ -142,12 +176,11 @@ postcomp-hom-Category :
 postcomp-hom-Category C = postcomp-hom-Precategory (precategory-Category C)
 ```
 
-### Equalities give rise to homomorphisms
+### Equalities induce morphisms
 
 ```agda
 module _
-  {l1 l2 : Level}
-  (C : Category l1 l2)
+  {l1 l2 : Level} (C : Category l1 l2)
   where
 
   hom-eq-Category :
@@ -173,14 +206,10 @@ module _
   where
 
   is-1-type-obj-Category : is-1-type (obj-Category C)
-  is-1-type-obj-Category x y =
-    is-set-is-equiv
-      ( iso-Precategory (precategory-Category C) x y)
-      ( iso-eq-Precategory (precategory-Category C) x y)
-      ( is-category-Category C x y)
-      ( is-set-iso-Precategory (precategory-Category C))
+  is-1-type-obj-Category =
+    is-1-type-obj-Preunivalent-Category (preunivalent-category-Category C)
 
   obj-1-type-Category : 1-Type l1
-  pr1 obj-1-type-Category = obj-Category C
-  pr2 obj-1-type-Category = is-1-type-obj-Category
+  obj-1-type-Category =
+    obj-1-type-Preunivalent-Category (preunivalent-category-Category C)
 ```