Some extensions of the fundamental theorem of identity types

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},

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

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

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) →

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