Opposite categories, gaunt categories, replete subprecategories, large Yoneda, and miscellaneous additions

TEMPLATE.lagda.md

@@ -55,5 +55,4 @@ concept-subconcept = ...
 
 1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
    of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
-   [arXiv:1308.0729](https://arxiv.org/abs/1308.0729),
-   [DOI:10.48550](https://doi.org/10.48550/arXiv.1308.0729))
+   [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))

src/category-theory.lagda.md

@@ -59,6 +59,7 @@ open import category-theory.functors-from-small-to-large-precategories public
 open import category-theory.functors-large-categories public
 open import category-theory.functors-large-precategories public
 open import category-theory.functors-precategories public
+open import category-theory.gaunt-categories public
 open import category-theory.groupoids public
 open import category-theory.homotopies-natural-transformations-large-precategories public
 open import category-theory.initial-objects-large-categories public
@@ -70,6 +71,7 @@ open import category-theory.isomorphisms-in-categories public
 open import category-theory.isomorphisms-in-large-categories public
 open import category-theory.isomorphisms-in-large-precategories public
 open import category-theory.isomorphisms-in-precategories public
+open import category-theory.isomorphisms-in-subprecategories public
 open import category-theory.large-categories public
 open import category-theory.large-function-categories public
 open import category-theory.large-function-precategories public
@@ -97,7 +99,9 @@ open import category-theory.natural-transformations-maps-from-small-to-large-pre
 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-precategories public
+open import category-theory.opposite-preunivalent-categories public
 open import category-theory.precategories public
 open import category-theory.precategory-of-functors public
 open import category-theory.precategory-of-functors-from-small-to-large-precategories public
@@ -109,6 +113,7 @@ open import category-theory.preunivalent-categories public
 open import category-theory.products-in-precategories public
 open import category-theory.products-of-precategories public
 open import category-theory.pullbacks-in-precategories public
+open import category-theory.replete-subprecategories public
 open import category-theory.representable-functors-categories public
 open import category-theory.representable-functors-large-precategories public
 open import category-theory.representable-functors-precategories public

src/category-theory/categories.lagda.md

@@ -14,11 +14,13 @@ open import category-theory.precategories
 open import category-theory.preunivalent-categories
 
 open import foundation.1-types
+open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.surjective-maps
 open import foundation.universe-levels
 ```
 
@@ -56,6 +58,10 @@ module _
 
   is-category-Precategory : UU (l1 ⊔ l2)
   is-category-Precategory = type-Prop is-category-prop-Precategory
+
+  is-prop-is-category-Precategory : is-prop is-category-Precategory
+  is-prop-is-category-Precategory =
+    is-prop-type-Prop is-category-prop-Precategory
 ```
 
 ### The type of categories
@@ -156,6 +162,20 @@ module _
     is-emb-is-equiv (is-category-Category C x y)
 ```
 
+### The total hom-type of a preunivalent category
+
+```agda
+total-hom-Category :
+  {l1 l2 : Level} (C : Category l1 l2) → UU (l1 ⊔ l2)
+total-hom-Category C = total-hom-Precategory (precategory-Category C)
+
+obj-total-hom-Category :
+  {l1 l2 : Level} (C : Category l1 l2) →
+  total-hom-Category C →
+  obj-Category C × obj-Category C
+obj-total-hom-Category C = obj-total-hom-Precategory (precategory-Category C)
+```
+
 ### Equalities induce morphisms
 
 ```agda
@@ -207,3 +227,104 @@ module _
   obj-1-type-Category =
     obj-1-type-Preunivalent-Category (preunivalent-category-Category C)
 ```
+
+### The total hom-type of a category is a 1-type
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2)
+  where
+
+  is-1-type-total-hom-Category :
+    is-1-type (total-hom-Category C)
+  is-1-type-total-hom-Category =
+    is-1-type-total-hom-Preunivalent-Category (preunivalent-category-Category C)
+
+  total-hom-1-type-Category : 1-Type (l1 ⊔ l2)
+  total-hom-1-type-Category =
+    total-hom-1-type-Preunivalent-Category (preunivalent-category-Category C)
+```
+
+### A preunivalent category is a category if and only if `iso-eq` is surjective
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  where
+
+  is-surjective-iso-eq-prop-Precategory : Prop (l1 ⊔ l2)
+  is-surjective-iso-eq-prop-Precategory =
+    Π-Prop
+      ( obj-Precategory C)
+      ( λ x →
+        Π-Prop
+          ( obj-Precategory C)
+          ( λ y →
+            is-surjective-Prop
+              ( iso-eq-Precategory C x y)))
+
+  is-surjective-iso-eq-Precategory : UU (l1 ⊔ l2)
+  is-surjective-iso-eq-Precategory =
+    type-Prop is-surjective-iso-eq-prop-Precategory
+
+  is-prop-is-surjective-iso-eq-Precategory :
+    is-prop is-surjective-iso-eq-Precategory
+  is-prop-is-surjective-iso-eq-Precategory =
+    is-prop-type-Prop is-surjective-iso-eq-prop-Precategory
+```
+
+```agda
+module _
+  {l1 l2 : Level} (C : Preunivalent-Category l1 l2)
+  where
+
+  is-category-is-surjective-iso-eq-Preunivalent-Category :
+    is-surjective-iso-eq-Precategory (precategory-Preunivalent-Category C) →
+    is-category-Precategory (precategory-Preunivalent-Category C)
+  is-category-is-surjective-iso-eq-Preunivalent-Category
+    is-surjective-iso-eq-C x y =
+    is-equiv-is-emb-is-surjective
+      ( is-surjective-iso-eq-C x y)
+      ( is-preunivalent-Preunivalent-Category C x y)
+
+  is-surjective-iso-eq-is-category-Preunivalent-Category :
+    is-category-Precategory (precategory-Preunivalent-Category C) →
+    is-surjective-iso-eq-Precategory (precategory-Preunivalent-Category C)
+  is-surjective-iso-eq-is-category-Preunivalent-Category
+    is-category-C x y =
+    is-surjective-is-equiv (is-category-C x y)
+
+  is-equiv-is-category-is-surjective-iso-eq-Preunivalent-Category :
+    is-equiv is-category-is-surjective-iso-eq-Preunivalent-Category
+  is-equiv-is-category-is-surjective-iso-eq-Preunivalent-Category =
+    is-equiv-is-prop
+      ( is-prop-is-surjective-iso-eq-Precategory
+        ( precategory-Preunivalent-Category C))
+      ( is-prop-is-category-Precategory (precategory-Preunivalent-Category C))
+      ( is-surjective-iso-eq-is-category-Preunivalent-Category)
+
+  is-equiv-is-surjective-iso-eq-is-category-Preunivalent-Category :
+    is-equiv is-surjective-iso-eq-is-category-Preunivalent-Category
+  is-equiv-is-surjective-iso-eq-is-category-Preunivalent-Category =
+    is-equiv-is-prop
+      ( is-prop-is-category-Precategory (precategory-Preunivalent-Category C))
+      ( is-prop-is-surjective-iso-eq-Precategory
+        ( precategory-Preunivalent-Category C))
+      ( is-category-is-surjective-iso-eq-Preunivalent-Category)
+
+  equiv-is-category-is-surjective-iso-eq-Preunivalent-Category :
+    is-surjective-iso-eq-Precategory (precategory-Preunivalent-Category C) ≃
+    is-category-Precategory (precategory-Preunivalent-Category C)
+  pr1 equiv-is-category-is-surjective-iso-eq-Preunivalent-Category =
+    is-category-is-surjective-iso-eq-Preunivalent-Category
+  pr2 equiv-is-category-is-surjective-iso-eq-Preunivalent-Category =
+    is-equiv-is-category-is-surjective-iso-eq-Preunivalent-Category
+
+  equiv-is-surjective-iso-eq-is-category-Preunivalent-Category :
+    is-category-Precategory (precategory-Preunivalent-Category C) ≃
+    is-surjective-iso-eq-Precategory (precategory-Preunivalent-Category C)
+  pr1 equiv-is-surjective-iso-eq-is-category-Preunivalent-Category =
+    is-surjective-iso-eq-is-category-Preunivalent-Category
+  pr2 equiv-is-surjective-iso-eq-is-category-Preunivalent-Category =
+    is-equiv-is-surjective-iso-eq-is-category-Preunivalent-Category
+```

src/category-theory/coproducts-in-precategories.lagda.md

@@ -14,6 +14,7 @@ open import foundation.cartesian-product-types
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types
+open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.unique-existence
 open import foundation.universe-levels
@@ -121,7 +122,7 @@ module _
   is-prop-is-coproduct-Precategory :
     is-prop (is-coproduct-Precategory C x y p l r)
   is-prop-is-coproduct-Precategory =
-    is-prop-Π³ (λ z f g → is-property-is-contr)
+    is-prop-iterated-Π 3 (λ z f g → is-property-is-contr)
 
   is-coproduct-prop-Precategory : Prop (l1 ⊔ l2)
   pr1 is-coproduct-prop-Precategory = is-coproduct-Precategory C x y p l r

src/category-theory/faithful-maps-precategories.lagda.md

@@ -15,6 +15,7 @@ open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.injective-maps
+open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.universe-levels
 ```
@@ -49,7 +50,8 @@ module _
 
   is-prop-is-faithful-map-Precategory : is-prop is-faithful-map-Precategory
   is-prop-is-faithful-map-Precategory =
-    is-prop-Π² (λ x y → is-prop-is-emb (hom-map-Precategory C D F {x} {y}))
+    is-prop-iterated-Π 2
+      ( λ x y → is-property-is-emb (hom-map-Precategory C D F {x} {y}))
 
   is-faithful-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4)
   pr1 is-faithful-prop-map-Precategory = is-faithful-map-Precategory
@@ -110,7 +112,7 @@ module _
   is-prop-is-injective-hom-map-Precategory :
     is-prop is-injective-hom-map-Precategory
   is-prop-is-injective-hom-map-Precategory =
-    is-prop-Π²
+    is-prop-iterated-Π 2
       ( λ x y →
         is-prop-is-injective
           ( is-set-hom-Precategory C x y)

src/category-theory/full-maps-precategories.lagda.md

@@ -12,6 +12,7 @@ open import category-theory.precategories
 
 open import foundation.dependent-pair-types
 open import foundation.function-types
+open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.surjective-maps
 open import foundation.universe-levels
@@ -45,7 +46,7 @@ module _
 
   is-prop-is-full-map-Precategory : is-prop is-full-map-Precategory
   is-prop-is-full-map-Precategory =
-    is-prop-Π²
+    is-prop-iterated-Π 2
       ( λ x y → is-prop-is-surjective (hom-map-Precategory C D F {x} {y}))
 
   is-full-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4)

src/category-theory/fully-faithful-maps-precategories.lagda.md

@@ -15,6 +15,7 @@ open import category-theory.precategories
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.function-types
+open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.surjective-maps
 open import foundation.universe-levels
@@ -50,7 +51,7 @@ module _
   is-prop-is-fully-faithful-map-Precategory :
     is-prop is-fully-faithful-map-Precategory
   is-prop-is-fully-faithful-map-Precategory =
-    is-prop-Π²
+    is-prop-iterated-Π 2
       ( λ x y → is-property-is-equiv (hom-map-Precategory C D F {x} {y}))
 
   is-fully-faithful-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4)