Refactor category theory to use strictly involutive identity types (#1052)

### Summary
- Refactors the definition of categories to use the new and more general
strictly involutive identity types for their associativity witnesses.
- Refactor definitions of some instances of large and small
precategories to use a new `make-(Large-)?-Precategory` constructor.
- Defines the underlying large precategory of a large subprecategory.
- Change some prose regarding basic definitions in category theory.
- Refactors all appropriate instances of large precategories to be
(full) large subprecategories.
  - Rename `is-group` to `is-group-Semigroup`.
 
The last item was appropriate to make the handling of
`involutive-eq-associative-comp-hom-***-Large-Precategory` systematic.

Improves on what was implemented in #945.

Author: fredrik-bakke

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

@@ -16,6 +16,7 @@ open import elementary-number-theory.natural-numbers
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.sets
+open import foundation.strictly-involutive-identity-types
 open import foundation.universe-levels
 
 open import order-theory.order-preserving-maps-posets
@@ -81,19 +82,19 @@ associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s} =
     ( Fin-Poset r)
     ( Fin-Poset s)
 
-inv-associative-comp-hom-augmented-simplex-Category :
+involutive-eq-associative-comp-hom-augmented-simplex-Category :
   {n m r s : obj-augmented-simplex-Category}
   (h : hom-augmented-simplex-Category r s)
   (g : hom-augmented-simplex-Category m r)
   (f : hom-augmented-simplex-Category n m) →
-  comp-hom-augmented-simplex-Category {n} {r} {s}
-    ( h)
-    ( comp-hom-augmented-simplex-Category {n} {m} {r} g f) ＝
   comp-hom-augmented-simplex-Category {n} {m} {s}
     ( comp-hom-augmented-simplex-Category {m} {r} {s} h g)
-    ( f)
-inv-associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s} =
-  inv-associative-comp-hom-Poset
+    ( f) ＝ⁱ
+  comp-hom-augmented-simplex-Category {n} {r} {s}
+    ( h)
+    ( comp-hom-augmented-simplex-Category {n} {m} {r} g f)
+involutive-eq-associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s} =
+  involutive-eq-associative-comp-hom-Poset
     ( Fin-Poset n)
     ( Fin-Poset m)
     ( Fin-Poset r)
@@ -104,16 +105,9 @@ associative-composition-operation-augmented-simplex-Category :
     hom-set-augmented-simplex-Category
 pr1 associative-composition-operation-augmented-simplex-Category {n} {m} {r} =
   comp-hom-augmented-simplex-Category {n} {m} {r}
-pr1
-  ( pr2
-      associative-composition-operation-augmented-simplex-Category
-        { n} {m} {r} {s} h g f) =
-  associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s} h g f
-pr2
-  ( pr2
-      associative-composition-operation-augmented-simplex-Category
-        { n} {m} {r} {s} h g f) =
-  inv-associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s} h g f
+pr2 associative-composition-operation-augmented-simplex-Category
+  { n} {m} {r} {s} =
+  involutive-eq-associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s}
 
 id-hom-augmented-simplex-Category :
   (n : obj-augmented-simplex-Category) → hom-augmented-simplex-Category n n

src/category-theory/categories.lagda.md

@@ -20,6 +20,7 @@ open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.strictly-involutive-identity-types
 open import foundation.surjective-maps
 open import foundation.universe-levels
 ```
@@ -28,7 +29,7 @@ open import foundation.universe-levels
 
 ## Idea
 
-A **category** in Homotopy Type Theory is a
+A {{#concept "category" Agda=Category}} in Homotopy Type Theory is a
 [precategory](category-theory.precategories.md) for which the
 [identifications](foundation-core.identity-types.md) between the objects are the
 [isomorphisms](category-theory.isomorphisms-in-precategories.md). More
@@ -105,15 +106,15 @@ module _
   associative-comp-hom-Category =
     associative-comp-hom-Precategory precategory-Category
 
-  inv-associative-comp-hom-Category :
+  involutive-eq-associative-comp-hom-Category :
     {x y z w : obj-Category}
     (h : hom-Category z w)
     (g : hom-Category y z)
     (f : hom-Category x y) →
-    comp-hom-Category h (comp-hom-Category g f) ＝
-    comp-hom-Category (comp-hom-Category h g) f
-  inv-associative-comp-hom-Category =
-    inv-associative-comp-hom-Precategory precategory-Category
+    comp-hom-Category (comp-hom-Category h g) f ＝ⁱ
+    comp-hom-Category h (comp-hom-Category g f)
+  involutive-eq-associative-comp-hom-Category =
+    involutive-eq-associative-comp-hom-Precategory precategory-Category
 
   associative-composition-operation-Category :
     associative-composition-operation-binary-family-Set hom-set-Category

src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md

@@ -14,6 +14,7 @@ open import foundation.identity-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.strictly-involutive-identity-types
 open import foundation.subtypes
 open import foundation.universe-levels
 ```
@@ -22,22 +23,24 @@ open import foundation.universe-levels
 
 ## Idea
 
-Given a type `A`, a **composition operation on a binary family of sets**
-`hom : A → A → Set ` is a map
+Given a type `A`, a
+{{#concept "composition operation" Disambiguation="on binary families of sets" Agda=composition-operation-binary-family-Set}}
+on a binary family of [sets](foundation-core.sets.md) `hom : A → A → Set` is a
+map
 
 ```text
-  hom y z → hom x y → hom x z
+  _∘_ : hom y z → hom x y → hom x z
 ```
 
 for every triple of elements `x y z : A`.
 
 For such operations, we can consider
-[properties](foundation-core.propositions.md) such as **associativity** and
-**unitality**.
+[properties](foundation-core.propositions.md) such as _associativity_ and
+_unitality_.
 
 ## Definitions
 
-### Composition operations in binary families of sets
+### Composition operations on binary families of sets
 
 ```agda
 module _
@@ -50,14 +53,30 @@ module _
     type-Set (hom-set y z) → type-Set (hom-set x y) → type-Set (hom-set x z)
 ```
 
-### Associative composition operations in binary families of sets
+### Associative composition operations on binary families of sets
 
-We give a slightly nonstandard definition of associativity, requiring an
-associativity witness in each direction. This is of course redundant as `inv` is
-a [fibered involution](foundation.fibered-involutions.md) on
-[identity types](foundation-core.identity-types.md). However, by recording both
-directions we maintain a definitional double inverse law which is practical in
-defining the [opposite category](category-theory.opposite-categories.md).
+A composition operation
+
+```text
+  _∘_ : hom y z → hom x y → hom x z
+```
+
+on a binary family of sets of morphisms is called
+{{#concept "associative" Disambiguation="composition operation on a binary family of sets" Agda=is-associative-composition-operation-binary-family-Set}}
+if, for every triple of composable morphisms we have
+
+```text
+  (h ∘ g) ∘ f ＝ h ∘ (g ∘ f).
+```
+
+We give a slightly nonstandard definition of associativity using the
+[strictly involutive identity types](foundation.strictly-involutive-identity-types.md)
+rather than the standard [identity types](foundation-core.identity-types.md).
+This is because, while the strictly involutive identity types are always
+[equivalent](foundation-core.equivalences.md) to the standard ones, they satisfy
+the strict computation rule `inv (inv p) ≐ p` which is practical in defining the
+[opposite category](category-theory.opposite-categories.md), as this also makes
+the opposite construction strictly involutive: `(𝒞ᵒᵖ)ᵒᵖ ≐ 𝒞`.
 
 ```agda
 module _
@@ -71,8 +90,7 @@ module _
     (h : type-Set (hom-set z w))
     (g : type-Set (hom-set y z))
     (f : type-Set (hom-set x y)) →
-    ( comp-hom (comp-hom h g) f ＝ comp-hom h (comp-hom g f)) ×
-    ( comp-hom h (comp-hom g f) ＝ comp-hom (comp-hom h g) f)
+    ( comp-hom (comp-hom h g) f ＝ⁱ comp-hom h (comp-hom g f))
 
   associative-composition-operation-binary-family-Set : UU (l1 ⊔ l2)
   associative-composition-operation-binary-family-Set =
@@ -88,6 +106,19 @@ module _
     composition-operation-binary-family-Set hom-set
   comp-hom-associative-composition-operation-binary-family-Set = pr1 H
 
+  involutive-eq-associative-composition-operation-binary-family-Set :
+    {x y z w : A}
+    (h : type-Set (hom-set z w))
+    (g : type-Set (hom-set y z))
+    (f : type-Set (hom-set x y)) →
+    ( comp-hom-associative-composition-operation-binary-family-Set
+      ( comp-hom-associative-composition-operation-binary-family-Set h g)
+      ( f)) ＝ⁱ
+    ( comp-hom-associative-composition-operation-binary-family-Set
+      ( h)
+      ( comp-hom-associative-composition-operation-binary-family-Set g f))
+  involutive-eq-associative-composition-operation-binary-family-Set = pr2 H
+
   witness-associative-composition-operation-binary-family-Set :
     {x y z w : A}
     (h : type-Set (hom-set z w))
@@ -98,7 +129,8 @@ module _
     ( comp-hom-associative-composition-operation-binary-family-Set
       ( h) (comp-hom-associative-composition-operation-binary-family-Set g f))
   witness-associative-composition-operation-binary-family-Set h g f =
-    pr1 (pr2 H h g f)
+    eq-involutive-eq
+      ( involutive-eq-associative-composition-operation-binary-family-Set h g f)
 
   inv-witness-associative-composition-operation-binary-family-Set :
     {x y z w : A}
@@ -110,50 +142,32 @@ module _
     ( comp-hom-associative-composition-operation-binary-family-Set
       ( comp-hom-associative-composition-operation-binary-family-Set h g) (f))
   inv-witness-associative-composition-operation-binary-family-Set h g f =
-    pr2 (pr2 H h g f)
+    eq-involutive-eq
+      ( invⁱ
+        ( involutive-eq-associative-composition-operation-binary-family-Set
+          ( h)
+          ( g)
+          ( f)))
 ```
 
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1}
-  (hom-set : A → A → Set l2)
-  (comp-hom : composition-operation-binary-family-Set hom-set)
-  where
+### Unital composition operations on binary families of sets
 
-  is-associative-witness-associative-composition-operation-binary-family-Set :
-    ( {x y z w : A}
-      (h : type-Set (hom-set z w))
-      (g : type-Set (hom-set y z))
-      (f : type-Set (hom-set x y)) →
-      comp-hom (comp-hom h g) f ＝ comp-hom h (comp-hom g f)) →
-    is-associative-composition-operation-binary-family-Set hom-set comp-hom
-  pr1
-    ( is-associative-witness-associative-composition-operation-binary-family-Set
-        H h g f) =
-    H h g f
-  pr2
-    ( is-associative-witness-associative-composition-operation-binary-family-Set
-        H h g f) =
-    inv (H h g f)
-
-  is-associative-inv-witness-associative-composition-operation-binary-family-Set :
-    ( {x y z w : A}
-      (h : type-Set (hom-set z w))
-      (g : type-Set (hom-set y z))
-      (f : type-Set (hom-set x y)) →
-      comp-hom h (comp-hom g f) ＝ comp-hom (comp-hom h g) f) →
-    is-associative-composition-operation-binary-family-Set hom-set comp-hom
-  pr1
-    ( is-associative-inv-witness-associative-composition-operation-binary-family-Set
-        H h g f) =
-    inv (H h g f)
-  pr2
-    ( is-associative-inv-witness-associative-composition-operation-binary-family-Set
-        H h g f) =
-    H h g f
+A composition operation
+
+```text
+  _∘_ : hom y z → hom x y → hom x z
+```
+
+on a binary family of sets of morphisms is called
+{{#concept "unital" Disambiguation="composition operation on a binary family of sets" Agda=is-unital-composition-operation-binary-family-Set}}
+if there is a morphism `id_x : hom x x` for every element `x : A` such that
+
+```text
+  id_y ∘ f ＝ f   and f ∘ id_x = f.
 ```
 
-### Unital composition operations in binary families of sets
+As will be demonstrated momentarily, every composition operation on a binary
+family of sets is unital in [at most one](foundation.subterminal-types.md) way.
 
 ```agda
 module _
@@ -171,7 +185,7 @@ module _
 
 ## Properties
 
-### Being associative is a property of composition operations in binary families of sets
+### Being associative is a property of composition operations on binary families of sets
 
 ```agda
 module _
@@ -187,15 +201,12 @@ module _
       ( λ x y z w →
         is-prop-iterated-Π 3
           ( λ h g f →
-            is-prop-product
+            is-prop-equiv
+              ( equiv-eq-involutive-eq)
               ( is-set-type-Set
                 ( hom-set x w)
                 ( comp-hom (comp-hom h g) f)
-                ( comp-hom h (comp-hom g f)))
-              ( is-set-type-Set
-                ( hom-set x w)
-                ( comp-hom h (comp-hom g f))
-                ( comp-hom (comp-hom h g) f))))
+                ( comp-hom h (comp-hom g f)))))
 
   is-associative-prop-composition-operation-binary-family-Set : Prop (l1 ⊔ l2)
   pr1 is-associative-prop-composition-operation-binary-family-Set =
@@ -204,7 +215,7 @@ module _
     is-prop-is-associative-composition-operation-binary-family-Set
 ```
 
-### Being unital is a property of composition operations in binary families of sets
+### Being unital is a property of composition operations on binary families of sets
 
 **Proof:** Suppose `e e' : (x : A) → hom-set x x` are both right and left units
 with regard to composition. It is enough to show that `e ＝ e'` since the right
@@ -266,7 +277,8 @@ module _
 
 - [Set-magmoids](category-theory.set-magmoids.md) capture the structure of
   composition operations on binary families of sets.
-- [Precategories](category-theory.precategories.md) are associative and unital
-  composition operations on binary families of sets.
-- [Nonunital precategories](category-theory.nonunital-precategories.md) are
-  associative composition operations on binary families of sets.
+- [Precategories](category-theory.precategories.md) are the structure of an
+  associative and unital composition operation on a binary families of sets.
+- [Nonunital precategories](category-theory.nonunital-precategories.md) are the
+  structure of an associative composition operation on a binary families of
+  sets.

src/category-theory/conservative-functors-precategories.lagda.md

@@ -29,7 +29,7 @@ isomorphism in `C`.
 
 ## Definitions
 
-### The predicate of being conservative
+### The predicate on functors of being conservative
 
 ```agda
 module _

src/category-theory/copresheaf-categories.lagda.md

@@ -10,7 +10,6 @@ module category-theory.copresheaf-categories where
 open import category-theory.categories
 open import category-theory.category-of-functors-from-small-to-large-categories
 open import category-theory.functors-from-small-to-large-precategories
-open import category-theory.functors-precategories
 open import category-theory.large-categories
 open import category-theory.large-precategories
 open import category-theory.natural-transformations-functors-from-small-to-large-precategories
@@ -210,29 +209,6 @@ module _
       { Z}
       { W}
 
-  inv-associative-comp-hom-copresheaf-Precategory :
-    {l3 l4 l5 l6 : Level}
-    (X : copresheaf-Precategory l3)
-    (Y : copresheaf-Precategory l4)
-    (Z : copresheaf-Precategory l5)
-    (W : copresheaf-Precategory l6)
-    (h : hom-copresheaf-Precategory Z W)
-    (g : hom-copresheaf-Precategory Y Z)
-    (f : hom-copresheaf-Precategory X Y) →
-    comp-hom-copresheaf-Precategory X Z W
-      ( h)
-      ( comp-hom-copresheaf-Precategory X Y Z g f) ＝
-    comp-hom-copresheaf-Precategory X Y W
-      ( comp-hom-copresheaf-Precategory Y Z W h g)
-      ( f)
-  inv-associative-comp-hom-copresheaf-Precategory X Y Z W =
-    inv-associative-comp-hom-Large-Precategory
-      ( copresheaf-large-precategory-Precategory)
-      { X = X}
-      { Y}
-      { Z}
-      { W}
-
   left-unit-law-comp-hom-copresheaf-Precategory :
     {l3 l4 : Level}
     (X : copresheaf-Precategory l3)