Refactor categories to carry a bidirectional witness of associativity (…

…#945)

src/category-theory.lagda.md

@@ -115,6 +115,7 @@ 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-categories public
+open import category-theory.opposite-large-precategories public
 open import category-theory.opposite-precategories public
 open import category-theory.opposite-preunivalent-categories public
 open import category-theory.precategories public

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

@@ -68,27 +68,52 @@ associative-comp-hom-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} {m} {s}
+  comp-hom-augmented-simplex-Category {n} {m} {s}
     ( comp-hom-augmented-simplex-Category {m} {r} {s} h g)
-    ( f)) ＝
-  ( comp-hom-augmented-simplex-Category {n} {r} {s}
+    ( f) ＝
+  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} {r} g f)
 associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s} =
   associative-comp-hom-Poset
     ( Fin-Poset n)
     ( Fin-Poset m)
     ( Fin-Poset r)
     ( Fin-Poset s)
 
+inv-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
+    ( Fin-Poset n)
+    ( Fin-Poset m)
+    ( Fin-Poset r)
+    ( Fin-Poset s)
+
 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}
+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
-  associative-composition-operation-augmented-simplex-Category {n} {m} {r} {s} =
-  associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s}
+  ( 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
 
 id-hom-augmented-simplex-Category :
   (n : obj-augmented-simplex-Category) → hom-augmented-simplex-Category n n

src/category-theory/categories.lagda.md

@@ -105,6 +105,16 @@ module _
   associative-comp-hom-Category =
     associative-comp-hom-Precategory precategory-Category
 
+  inv-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
+
   associative-composition-operation-Category :
     associative-composition-operation-binary-family-Set hom-set-Category
   associative-composition-operation-Category =

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

@@ -52,6 +52,13 @@ module _
 
 ### Associative composition operations in binary families of sets
 
+We give a slightly non-standard 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).
+
 ```agda
 module _
   {l1 l2 : Level} {A : UU l1} (hom-set : A → A → Set l2)
@@ -64,12 +71,86 @@ 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 (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)
 
   associative-composition-operation-binary-family-Set : UU (l1 ⊔ l2)
   associative-composition-operation-binary-family-Set =
     Σ ( composition-operation-binary-family-Set hom-set)
       ( is-associative-composition-operation-binary-family-Set)
+
+module _
+  {l1 l2 : Level} {A : UU l1} (hom-set : A → A → Set l2)
+  (H : associative-composition-operation-binary-family-Set hom-set)
+  where
+
+  comp-hom-associative-composition-operation-binary-family-Set :
+    composition-operation-binary-family-Set hom-set
+  comp-hom-associative-composition-operation-binary-family-Set = pr1 H
+
+  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-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))
+  witness-associative-composition-operation-binary-family-Set h g f =
+    pr1 (pr2 H h g f)
+
+  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-associative-composition-operation-binary-family-Set
+      ( h) (comp-hom-associative-composition-operation-binary-family-Set g f)) ＝
+    ( 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)
+```
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1}
+  (hom-set : A → A → Set l2)
+  (comp-hom : composition-operation-binary-family-Set hom-set)
+  where
+
+  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
 ```
 
 ### Unital composition operations in binary families of sets
@@ -106,10 +187,15 @@ module _
       ( λ x y z w →
         is-prop-iterated-Π 3
           ( λ h g f →
-            is-set-type-Set
-              ( hom-set x w)
-              ( comp-hom (comp-hom h g) f)
-              ( comp-hom h (comp-hom g f))))
+            is-prop-prod
+              ( 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))))
 
   is-associative-prop-composition-operation-binary-family-Set : Prop (l1 ⊔ l2)
   pr1 is-associative-prop-composition-operation-binary-family-Set =

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

@@ -124,6 +124,29 @@ module _
       { Z}
       { W}
 
+  inv-associative-comp-hom-copresheaf-Large-Category :
+    {l3 l4 l5 l6 : Level}
+    (X : obj-copresheaf-Large-Category l3)
+    (Y : obj-copresheaf-Large-Category l4)
+    (Z : obj-copresheaf-Large-Category l5)
+    (W : obj-copresheaf-Large-Category l6)
+    (h : hom-copresheaf-Large-Category Z W)
+    (g : hom-copresheaf-Large-Category Y Z)
+    (f : hom-copresheaf-Large-Category X Y) →
+    comp-hom-copresheaf-Large-Category X Z W
+      ( h)
+      ( comp-hom-copresheaf-Large-Category X Y Z g f) ＝
+    comp-hom-copresheaf-Large-Category X Y W
+      ( comp-hom-copresheaf-Large-Category Y Z W h g)
+      ( f)
+  inv-associative-comp-hom-copresheaf-Large-Category X Y Z W =
+    inv-associative-comp-hom-Large-Precategory
+      ( copresheaf-Large-Precategory)
+      { X = X}
+      { Y}
+      { Z}
+      { W}
+
   left-unit-law-comp-hom-copresheaf-Large-Category :
     {l3 l4 : Level}
     (X : obj-copresheaf-Large-Category l3)

src/category-theory/dependent-products-of-categories.lagda.md

@@ -80,11 +80,21 @@ module _
     (h : hom-Π-Category z w)
     (g : hom-Π-Category y z)
     (f : hom-Π-Category x y) →
-    ( comp-hom-Π-Category (comp-hom-Π-Category h g) f) ＝
-    ( comp-hom-Π-Category h (comp-hom-Π-Category g f))
+    comp-hom-Π-Category (comp-hom-Π-Category h g) f ＝
+    comp-hom-Π-Category h (comp-hom-Π-Category g f)
   associative-comp-hom-Π-Category =
     associative-comp-hom-Category Π-Category
 
+  inv-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-Category Π-Category
+
   associative-composition-operation-Π-Category :
     associative-composition-operation-binary-family-Set hom-set-Π-Category
   associative-composition-operation-Π-Category =

src/category-theory/dependent-products-of-large-categories.lagda.md

@@ -93,11 +93,25 @@ module _
     (h : hom-Π-Large-Category z w)
     (g : hom-Π-Large-Category y z)
     (f : hom-Π-Large-Category x y) →
-    ( comp-hom-Π-Large-Category (comp-hom-Π-Large-Category h g) f) ＝
-    ( comp-hom-Π-Large-Category h (comp-hom-Π-Large-Category g f))
+    comp-hom-Π-Large-Category (comp-hom-Π-Large-Category h g) f ＝
+    comp-hom-Π-Large-Category h (comp-hom-Π-Large-Category g f)
   associative-comp-hom-Π-Large-Category =
     associative-comp-hom-Large-Category Π-Large-Category
 
+  inv-associative-comp-hom-Π-Large-Category :
+    {l2 l3 l4 l5 : Level}
+    {x : obj-Π-Large-Category l2}
+    {y : obj-Π-Large-Category l3}
+    {z : obj-Π-Large-Category l4}
+    {w : obj-Π-Large-Category l5} →
+    (h : hom-Π-Large-Category z w)
+    (g : hom-Π-Large-Category y z)
+    (f : hom-Π-Large-Category x y) →
+    comp-hom-Π-Large-Category h (comp-hom-Π-Large-Category g f) ＝
+    comp-hom-Π-Large-Category (comp-hom-Π-Large-Category h g) f
+  inv-associative-comp-hom-Π-Large-Category =
+    inv-associative-comp-hom-Large-Category Π-Large-Category
+
   id-hom-Π-Large-Category :
     {l2 : Level} {x : obj-Π-Large-Category l2} →
     hom-Π-Large-Category x x

src/category-theory/dependent-products-of-large-precategories.lagda.md

@@ -77,6 +77,22 @@ module _
     eq-htpy
       ( λ i → associative-comp-hom-Large-Precategory (C i) (h i) (g i) (f i))
 
+  inv-associative-comp-hom-Π-Large-Precategory :
+    {l2 l3 l4 l5 : Level}
+    {x : obj-Π-Large-Precategory l2}
+    {y : obj-Π-Large-Precategory l3}
+    {z : obj-Π-Large-Precategory l4}
+    {w : obj-Π-Large-Precategory l5} →
+    (h : hom-Π-Large-Precategory z w)
+    (g : hom-Π-Large-Precategory y z)
+    (f : hom-Π-Large-Precategory x y) →
+    ( comp-hom-Π-Large-Precategory h (comp-hom-Π-Large-Precategory g f)) ＝
+    ( comp-hom-Π-Large-Precategory (comp-hom-Π-Large-Precategory h g) f)
+  inv-associative-comp-hom-Π-Large-Precategory h g f =
+    eq-htpy
+      ( λ i →
+        inv-associative-comp-hom-Large-Precategory (C i) (h i) (g i) (f i))
+
   id-hom-Π-Large-Precategory :
     {l2 : Level} {x : obj-Π-Large-Precategory l2} → hom-Π-Large-Precategory x x
   id-hom-Π-Large-Precategory i = id-hom-Large-Precategory (C i)
@@ -101,26 +117,21 @@ module _
 
   Π-Large-Precategory :
     Large-Precategory (λ l2 → l1 ⊔ α l2) (λ l2 l3 → l1 ⊔ β l2 l3)
-  obj-Large-Precategory
-    Π-Large-Precategory =
+  obj-Large-Precategory Π-Large-Precategory =
     obj-Π-Large-Precategory
-  hom-set-Large-Precategory
-    Π-Large-Precategory =
+  hom-set-Large-Precategory Π-Large-Precategory =
     hom-set-Π-Large-Precategory
-  comp-hom-Large-Precategory
-    Π-Large-Precategory =
+  comp-hom-Large-Precategory Π-Large-Precategory =
     comp-hom-Π-Large-Precategory
-  id-hom-Large-Precategory
-    Π-Large-Precategory =
+  id-hom-Large-Precategory Π-Large-Precategory =
     id-hom-Π-Large-Precategory
-  associative-comp-hom-Large-Precategory
-    Π-Large-Precategory =
+  associative-comp-hom-Large-Precategory Π-Large-Precategory =
     associative-comp-hom-Π-Large-Precategory
-  left-unit-law-comp-hom-Large-Precategory
-    Π-Large-Precategory =
+  inv-associative-comp-hom-Large-Precategory Π-Large-Precategory =
+    inv-associative-comp-hom-Π-Large-Precategory
+  left-unit-law-comp-hom-Large-Precategory Π-Large-Precategory =
     left-unit-law-comp-hom-Π-Large-Precategory
-  right-unit-law-comp-hom-Large-Precategory
-    Π-Large-Precategory =
+  right-unit-law-comp-hom-Large-Precategory Π-Large-Precategory =
     right-unit-law-comp-hom-Π-Large-Precategory
 ```
 

src/category-theory/dependent-products-of-precategories.lagda.md

@@ -64,11 +64,23 @@ module _
   associative-comp-hom-Π-Precategory h g f =
     eq-htpy (λ i → associative-comp-hom-Precategory (C i) (h i) (g i) (f i))
 
+  inv-associative-comp-hom-Π-Precategory :
+    {x y z w : obj-Π-Precategory}
+    (h : hom-Π-Precategory z w)
+    (g : hom-Π-Precategory y z)
+    (f : hom-Π-Precategory x y) →
+    ( comp-hom-Π-Precategory h (comp-hom-Π-Precategory g f)) ＝
+    ( comp-hom-Π-Precategory (comp-hom-Π-Precategory h g) f)
+  inv-associative-comp-hom-Π-Precategory h g f =
+    eq-htpy (λ i → inv-associative-comp-hom-Precategory (C i) (h i) (g i) (f i))
+
   associative-composition-operation-Π-Precategory :
     associative-composition-operation-binary-family-Set hom-set-Π-Precategory
   pr1 associative-composition-operation-Π-Precategory = comp-hom-Π-Precategory
-  pr2 associative-composition-operation-Π-Precategory =
-    associative-comp-hom-Π-Precategory
+  pr1 (pr2 associative-composition-operation-Π-Precategory h g f) =
+    associative-comp-hom-Π-Precategory h g f
+  pr2 (pr2 associative-composition-operation-Π-Precategory h g f) =
+    inv-associative-comp-hom-Π-Precategory h g f
 
   id-hom-Π-Precategory : {x : obj-Π-Precategory} → hom-Π-Precategory x x
   id-hom-Π-Precategory i = id-hom-Precategory (C i)

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

@@ -32,7 +32,8 @@ module _
   pr1 (pr2 discrete-precategory-Set) x y =
     set-Prop (x ＝ y , is-set-type-Set X x y)
   pr1 (pr1 (pr2 (pr2 discrete-precategory-Set))) = concat' _
-  pr2 (pr1 (pr2 (pr2 discrete-precategory-Set))) refl refl refl = refl
+  pr1 (pr2 (pr1 (pr2 (pr2 discrete-precategory-Set))) refl refl refl) = refl
+  pr2 (pr2 (pr1 (pr2 (pr2 discrete-precategory-Set))) refl refl refl) = refl
   pr1 (pr2 (pr2 (pr2 discrete-precategory-Set))) x = refl
   pr1 (pr2 (pr2 (pr2 (pr2 discrete-precategory-Set)))) _ = right-unit
   pr2 (pr2 (pr2 (pr2 (pr2 discrete-precategory-Set)))) _ = left-unit