Merge branch 'master' into compact

UniMath · Nov 27, 2023 · 63048fd · 63048fd
2 parents b2982f4 + fe41f7e
commit 63048fd
Show file tree

Hide file tree

Showing 157 changed files with 5,272 additions and 1,095 deletions.
diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
@@ -115,9 +115,11 @@ 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
+open import category-theory.precategory-of-elements-of-a-presheaf public
 open import category-theory.precategory-of-functors public
 open import category-theory.precategory-of-functors-from-small-to-large-precategories public
 open import category-theory.precategory-of-maps-from-small-to-large-precategories public

diff --git a/src/category-theory/augmented-simplex-category.lagda.md b/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

diff --git a/src/category-theory/categories.lagda.md b/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 =

diff --git a/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md b/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 =