Some extensions of the fundamental theorem of identity types (#1243)

So my recent work on π₀-trivial types got me looking for other applications of this concept, and here's one. Essentially, this PR gives an alternative phrasing of the extended fundamental theorem of identity types such that the assumption of inhabitedness/pointedness on the base type `A` is not needed. Edit: the scope of this PR has grown since the above description was written. ### Summary - Unbased version of the extended fundamental theorem of identity types - Structured equality duality - Strong preunivalence - Strengthen definition of preunivalent categories - Weaken assumptions on the type theoretic Yoneda lemma
UniMath · Feb 10, 2025 · 8ba9c35 · 8ba9c35
1 parent a9ee070
commit 8ba9c35
Show file tree

Hide file tree

Showing 29 changed files with 1,408 additions and 302 deletions.
diff --git a/references.bib b/references.bib
@@ -320,6 +320,16 @@ @article{Esc08
   primaryclass = {cs.LO}
 }
 
+@online{Esc17YetAnother,
+  title        = {Yet another characterization of univalence},
+  author       = {Escardó, Martín Hötzel},
+  date         = {2017-11-18},
+  year         = {2017},
+  month        = {11},
+  url          = {https://groups.google.com/g/homotopytypetheory/c/FfiZj1vrkmQ/m/GJETdy0AAgAJ},
+  howpublished = {{{Google}} groups forum discussion}
+}
+
 @online{Esc19DefinitionsEquivalence,
   title        = {Definitions of Equivalence Satisfying Judgmental/Strict Groupoid Laws?},
   author       = {Escardó, Martín Hötzel},

diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
@@ -129,6 +129,7 @@ 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.opposite-strongly-preunivalent-categories public
 open import category-theory.pointed-endofunctors-categories public
 open import category-theory.pointed-endofunctors-precategories public
 open import category-theory.precategories public
@@ -160,6 +161,7 @@ open import category-theory.simplex-category public
 open import category-theory.slice-precategories public
 open import category-theory.split-essentially-surjective-functors-precategories public
 open import category-theory.strict-categories public
+open import category-theory.strongly-preunivalent-categories public
 open import category-theory.structure-equivalences-set-magmoids public
 open import category-theory.subcategories public
 open import category-theory.subprecategories public

diff --git a/src/category-theory/categories.lagda.md b/src/category-theory/categories.lagda.md
@@ -12,11 +12,13 @@ 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 category-theory.strongly-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.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.propositions
@@ -161,21 +163,24 @@ module _
     nonunital-precategory-Precategory (precategory-Category C)
 ```
 
-### The underlying preunivalent category of a category
+### The underlying strongly preunivalent category of a category
 
 ```agda
 module _
   {l1 l2 : Level} (C : Category l1 l2)
   where
 
-  is-preunivalent-category-Category :
-    is-preunivalent-Precategory (precategory-Category C)
-  is-preunivalent-category-Category x y =
-    is-emb-is-equiv (is-category-Category C x y)
-
-  preunivalent-category-Category : Preunivalent-Category l1 l2
-  pr1 preunivalent-category-Category = precategory-Category C
-  pr2 preunivalent-category-Category = is-preunivalent-category-Category
+  is-strongly-preunivalent-category-Category :
+    is-strongly-preunivalent-Precategory (precategory-Category C)
+  is-strongly-preunivalent-category-Category x =
+    is-set-is-contr
+      ( fundamental-theorem-id'
+        ( iso-eq-Precategory (precategory-Category C) x)
+        ( is-category-Category C x))
+
+  strongly-preunivalent-category-Category : Strongly-Preunivalent-Category l1 l2
+  strongly-preunivalent-category-Category =
+    ( precategory-Category C , is-strongly-preunivalent-category-Category)
 ```
 
 ### The total hom-type of a category
@@ -237,11 +242,13 @@ module _
 
   is-1-type-obj-Category : is-1-type (obj-Category C)
   is-1-type-obj-Category =
-    is-1-type-obj-Preunivalent-Category (preunivalent-category-Category C)
+    is-1-type-obj-Strongly-Preunivalent-Category
+      ( strongly-preunivalent-category-Category C)
 
   obj-1-type-Category : 1-Type l1
   obj-1-type-Category =
-    obj-1-type-Preunivalent-Category (preunivalent-category-Category C)
+    obj-1-type-Strongly-Preunivalent-Category
+      ( strongly-preunivalent-category-Category C)
 ```
 
 ### The total hom-type of a category is a 1-type
@@ -254,11 +261,13 @@ module _
   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)
+    is-1-type-total-hom-Strongly-Preunivalent-Category
+      ( strongly-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)
+    total-hom-1-type-Strongly-Preunivalent-Category
+      ( strongly-preunivalent-category-Category C)
 ```
 
 ### A preunivalent category is a category if and only if `iso-eq` is surjective

diff --git a/src/category-theory/gaunt-categories.lagda.md b/src/category-theory/gaunt-categories.lagda.md
@@ -14,16 +14,17 @@ open import category-theory.isomorphisms-in-categories
 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 category-theory.rigid-objects-categories
 open import category-theory.strict-categories
+open import category-theory.strongly-preunivalent-categories
 
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 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
 ```
 
@@ -55,7 +56,7 @@ diagram relating the different notions of "category":
           \           /
             \       /
               ∨   ∨
-      Preunivalent categories
+  Strongly Preunivalent categories
                 |
                 |
                 ∨
@@ -231,13 +232,13 @@ precategory-Gaunt-Category :
 precategory-Gaunt-Category C = precategory-Category (category-Gaunt-Category C)
 ```
 
-### The underlying preunivalent category of a gaunt category
+### The underlying strongly preunivalent category of a gaunt category
 
 ```agda
-preunivalent-category-Gaunt-Category :
-  {l1 l2 : Level} → Gaunt-Category l1 l2 → Preunivalent-Category l1 l2
-preunivalent-category-Gaunt-Category C =
-  preunivalent-category-Category (category-Gaunt-Category C)
+strongly-preunivalent-category-Gaunt-Category :
+  {l1 l2 : Level} → Gaunt-Category l1 l2 → Strongly-Preunivalent-Category l1 l2
+strongly-preunivalent-category-Gaunt-Category C =
+  strongly-preunivalent-category-Category (category-Gaunt-Category C)
 ```
 
 ### The total hom-type of a gaunt category
@@ -280,12 +281,13 @@ module _
 ### Preunivalent categories whose isomorphism-sets are propositions are strict categories
 
 ```agda
-is-strict-category-is-prop-iso-Preunivalent-Category :
-  {l1 l2 : Level} (C : Preunivalent-Category l1 l2) →
-  is-prop-iso-Precategory (precategory-Preunivalent-Category C) →
-  is-strict-category-Preunivalent-Category C
-is-strict-category-is-prop-iso-Preunivalent-Category C is-prop-iso-C x y =
-  is-prop-emb (emb-iso-eq-Preunivalent-Category C) (is-prop-iso-C x y)
+is-strict-category-is-prop-iso-Strongly-Preunivalent-Category :
+  {l1 l2 : Level} (C : Strongly-Preunivalent-Category l1 l2) →
+  is-prop-iso-Precategory (precategory-Strongly-Preunivalent-Category C) →
+  is-strict-category-Strongly-Preunivalent-Category C
+is-strict-category-is-prop-iso-Strongly-Preunivalent-Category
+  C is-prop-iso-C x y =
+  is-prop-emb (emb-iso-eq-Strongly-Preunivalent-Category C) (is-prop-iso-C x y)
 ```
 
 ### Gaunt categories are strict
@@ -295,8 +297,8 @@ is-strict-category-is-gaunt-Category :
   {l1 l2 : Level} (C : Category l1 l2) →
   is-gaunt-Category C → is-strict-category-Category C
 is-strict-category-is-gaunt-Category C =
-  is-strict-category-is-prop-iso-Preunivalent-Category
-    ( preunivalent-category-Category C)
+  is-strict-category-is-prop-iso-Strongly-Preunivalent-Category
+    ( strongly-preunivalent-category-Category C)
 ```
 
 ### A strict category is gaunt if `iso-eq` is surjective
@@ -309,9 +311,13 @@ module _
   is-category-is-surjective-iso-eq-Strict-Category :
     is-surjective-iso-eq-Precategory (precategory-Strict-Category C) →
     is-category-Precategory (precategory-Strict-Category C)
-  is-category-is-surjective-iso-eq-Strict-Category =
-    is-category-is-surjective-iso-eq-Preunivalent-Category
-      ( preunivalent-category-Strict-Category C)
+  is-category-is-surjective-iso-eq-Strict-Category H x y =
+    is-equiv-is-emb-is-surjective
+      ( H x y)
+      ( is-preunivalent-Strongly-Preunivalent-Category
+        ( strongly-preunivalent-category-Strict-Category C)
+        ( x)
+        ( y))
 
   is-prop-iso-is-category-Strict-Category :
     is-category-Precategory (precategory-Strict-Category C) →

diff --git a/src/category-theory/initial-category.lagda.md b/src/category-theory/initial-category.lagda.md
@@ -12,8 +12,8 @@ open import category-theory.functors-precategories
 open import category-theory.gaunt-categories
 open import category-theory.indiscrete-precategories
 open import category-theory.precategories
-open import category-theory.preunivalent-categories
 open import category-theory.strict-categories
+open import category-theory.strongly-preunivalent-categories
 
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
@@ -104,16 +104,16 @@ pr1 initial-Category = initial-Precategory
 pr2 initial-Category = is-category-initial-Category
 ```
 
-### The initial preunivalent category
+### The initial strongly preunivalent category
 
 ```agda
-is-preunivalent-initial-Category :
-  is-preunivalent-Precategory initial-Precategory
-is-preunivalent-initial-Category ()
+is-strongly-preunivalent-initial-Category :
+  is-strongly-preunivalent-Precategory initial-Precategory
+is-strongly-preunivalent-initial-Category ()
 
-initial-Preunivalent-Category : Preunivalent-Category lzero lzero
-initial-Preunivalent-Category =
-  preunivalent-category-Category initial-Category
+-- initial-Preunivalent-Category : Preunivalent-Category lzero lzero
+-- initial-Preunivalent-Category =
+--   strongly-preunivalent-category-Category initial-Category
 ```
 
 ### The initial strict category