Some extensions of the fundamental theorem of identity types

references.bib

@@ -304,6 +304,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/categories.lagda.md

@@ -17,6 +17,7 @@ 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
@@ -170,8 +171,11 @@ module _
 
   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)
+  is-preunivalent-category-Category x =
+    is-set-is-contr
+      ( fundamental-theorem-id'
+        ( iso-eq-Precategory (precategory-Category C) x)
+        ( is-category-Category C x))
 
   preunivalent-category-Category : Preunivalent-Category l1 l2
   pr1 preunivalent-category-Category = precategory-Category C
@@ -301,7 +305,7 @@ module _
     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)
+      ( preunivalence-Preunivalent-Category C x y)
 
   is-surjective-iso-eq-is-category-Preunivalent-Category :
     is-category-Precategory (precategory-Preunivalent-Category C) →

src/category-theory/indiscrete-precategories.lagda.md

@@ -212,7 +212,11 @@ module _
   is-strict-category-is-preunivalent-indiscrete-Precategory H x y =
     is-prop-is-emb
       ( iso-eq-Precategory (indiscrete-Precategory X) x y)
-      ( H x y)
+      ( preunivalence-is-preunivalent-Precategory
+        ( indiscrete-Precategory X)
+        ( H)
+        ( x)
+        ( y))
       ( is-prop-Σ
         ( is-prop-unit)
         ( is-prop-is-iso-Precategory (indiscrete-Precategory X) {x} {y}))

src/category-theory/opposite-preunivalent-categories.lagda.md

@@ -15,6 +15,7 @@ open import category-theory.preunivalent-categories
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
+open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.involutions
 open import foundation.sets
@@ -41,17 +42,13 @@ abstract
     {l1 l2 : Level} (C : Precategory l1 l2) →
     is-preunivalent-Precategory C →
     is-preunivalent-Precategory (opposite-Precategory C)
-  is-preunivalent-opposite-is-preunivalent-Precategory C is-preunivalent-C x y =
-    is-emb-htpy-emb
-      ( comp-emb
-        ( emb-equiv
-          ( compute-iso-opposite-Precategory C ∘e equiv-inv-iso-Precategory C))
-        ( _ , is-preunivalent-C x y))
-      ( λ where
-        refl →
-          eq-type-subtype
-            ( is-iso-prop-Precategory (opposite-Precategory C))
-            ( refl))
+  is-preunivalent-opposite-is-preunivalent-Precategory C is-preunivalent-C x =
+    is-set-equiv'
+      ( Σ (obj-opposite-Precategory C) (iso-Precategory C x))
+      ( equiv-tot
+        ( λ _ →
+          compute-iso-opposite-Precategory C ∘e equiv-inv-iso-Precategory C))
+      ( is-preunivalent-C x)
 
 abstract
   is-preunivalent-is-preunivalent-opposite-Precategory :

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

@@ -15,45 +15,46 @@ open import foundation.1-types
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.embeddings
+open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
+open import foundation.propositional-maps
 open import foundation.propositions
 open import foundation.sets
 open import foundation.strictly-involutive-identity-types
+open import foundation.structured-equality-duality
 open import foundation.universe-levels
 ```
 
 </details>
 
 ## Idea
 
-A **preunivalent category** is a [precategory](category-theory.precategories.md)
-for which the [identifications](foundation-core.identity-types.md) between the
-objects [embed](foundation-core.embeddings.md) into the
-[isomorphisms](category-theory.isomorphisms-in-precategories.md). More
-specifically, an equality between objects gives rise to an isomorphism between
-them, by the J-rule. A precategory is a preunivalent category if this function,
-called `iso-eq`, is an embedding.
-
-The idea of [preunivalence](foundation.preunivalence.md) is that it is a common
-generalization of univalent mathematics and mathematics with Axiom K. Hence
-preunivalent categories generalize both
-[(univalent) categories](category-theory.categories.md) and
+A {{#concept "preunivalent category" Agda=Preunivalent-Category}} `𝒞` is a
+[precategory](category-theory.precategories.md) for which every mapping of the
+concrete groupoid of objects into the groupoid of
+[isomorphisms](category-theory.isomorphisms-in-precategories.md) is an
+[embedding](foundation-core.embeddings.md). Equivalently, by
+[subuniverse equality duality](foundation.structured-equality-duality.md), a
+preunivalent category is a precategory whose based isomorphism types
+`Σ (x : 𝒞₀), (* ≅ x)` are [sets](foundation-core.sets.md).
+
+The main function of _preunivalence_ is to serve as a common generalization of
+univalent mathematics and mathematics with Axiom K by restricting the ways that
+identity and equivalence may interact. Hence preunivalent categories generalize
+both [(univalent) categories](category-theory.categories.md) and
 [strict categories](category-theory.strict-categories.md), which are
-precategories whose objects form a [set](foundation-core.sets.md).
-
-The preunivalence condition on precategories states that the type of objects is
-a subgroupoid of the [groupoid](category-theory.groupoids.md) of isomorphisms.
-For univalent categories the groupoid of objects is equivalent to the groupoid
-of isomorphisms, while for strict categories the groupoid of objects is
-discrete. Indeed, in this sense preunivalence provides a generalization of both
-notions of "category", with _no more structure_. This is opposed to the even
-more general notion of precategory, where the homotopy structure on the objects
-can be almost completely unrelated to the homotopy structure of the morphisms.
+precategories whose objects form a [set](foundation-core.sets.md). Note,
+however, that our definition of preunivalence here is a
+[strengthening](foundation.strong-preunivalence.md) of the
+[preunivalence axiom](foundation.preunivalence.md).
 
 ## Definitions
 
 ### The predicate on precategories of being a preunivalent category
 
+We define preunivalence of a precategory `𝒞` to be the condition that for every
+`x : 𝒞₀`, the type `Σ (y : 𝒞₀), (x ≅ y)` is a set.
+
 ```agda
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
@@ -64,12 +65,25 @@ module _
     Π-Prop
       ( obj-Precategory C)
       ( λ x →
-        Π-Prop
-          ( obj-Precategory C)
-          ( λ y → is-emb-Prop (iso-eq-Precategory C x y)))
+        is-set-Prop
+          ( Σ ( obj-Precategory C)
+              ( iso-Precategory C x)))
 
   is-preunivalent-Precategory : UU (l1 ⊔ l2)
   is-preunivalent-Precategory = type-Prop is-preunivalent-prop-Precategory
+
+  preunivalence-is-preunivalent-Precategory :
+    is-preunivalent-Precategory →
+    (x y : obj-Precategory C) →
+    is-emb (iso-eq-Precategory C x y)
+  preunivalence-is-preunivalent-Precategory H x y =
+    is-emb-is-prop-map
+      ( backward-implication-subuniverse-equality-duality
+        ( is-prop-Prop)
+        (H x)
+        ( x)
+        ( iso-eq-Precategory C x)
+        ( y))
 ```
 
 ### The type of preunivalent categories
@@ -168,13 +182,44 @@ module _
     is-preunivalent-Precategory precategory-Preunivalent-Category
   is-preunivalent-Preunivalent-Category = pr2 C
 
+  iso-Preunivalent-Category : (x y : obj-Preunivalent-Category) → UU l2
+  iso-Preunivalent-Category = iso-Precategory precategory-Preunivalent-Category
+
+  iso-eq-Preunivalent-Category :
+    (x y : obj-Preunivalent-Category) → x ＝ y → iso-Preunivalent-Category x y
+  iso-eq-Preunivalent-Category =
+    iso-eq-Precategory precategory-Preunivalent-Category
+
+  preunivalence-Preunivalent-Category :
+    (x y : obj-Preunivalent-Category) →
+    is-emb (iso-eq-Preunivalent-Category x y)
+  preunivalence-Preunivalent-Category =
+    preunivalence-is-preunivalent-Precategory
+      ( precategory-Preunivalent-Category)
+      ( is-preunivalent-Preunivalent-Category)
+
   emb-iso-eq-Preunivalent-Category :
     {x y : obj-Preunivalent-Category} →
     (x ＝ y) ↪ (iso-Precategory precategory-Preunivalent-Category x y)
-  pr1 (emb-iso-eq-Preunivalent-Category {x} {y}) =
-    iso-eq-Precategory precategory-Preunivalent-Category x y
-  pr2 (emb-iso-eq-Preunivalent-Category {x} {y}) =
-    is-preunivalent-Preunivalent-Category x y
+  emb-iso-eq-Preunivalent-Category {x} {y} =
+    ( iso-eq-Precategory precategory-Preunivalent-Category x y ,
+      preunivalence-Preunivalent-Category x y)
+```
+
+### The right-based isomorphism types of a preunivalent category are also sets
+
+```agda
+is-preunivalent-Preunivalent-Category' :
+  {l1 l2 : Level} (C : Preunivalent-Category l1 l2) →
+  ( x : obj-Preunivalent-Category C) →
+  is-set
+    ( Σ (obj-Preunivalent-Category C) (λ y → iso-Preunivalent-Category C y x))
+is-preunivalent-Preunivalent-Category' C x =
+  is-set-equiv
+    ( Σ (obj-Preunivalent-Category C) (iso-Preunivalent-Category C x))
+    ( equiv-tot
+      ( λ y → equiv-inv-iso-Precategory (precategory-Preunivalent-Category C)))
+    ( is-preunivalent-Preunivalent-Category C x)
 ```
 
 ### The total hom-type of a preunivalent category
@@ -255,7 +300,7 @@ module _
   is-1-type-obj-Preunivalent-Category x y =
     is-set-is-emb
       ( iso-eq-Precategory (precategory-Preunivalent-Category C) x y)
-      ( is-preunivalent-Preunivalent-Category C x y)
+      ( preunivalence-Preunivalent-Category C x y)
       ( is-set-iso-Precategory (precategory-Preunivalent-Category C))
 
   obj-1-type-Preunivalent-Category : 1-Type l1

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

@@ -192,12 +192,10 @@ module _
   abstract
     is-preunivalent-Strict-Category :
       is-preunivalent-Precategory (precategory-Strict-Category C)
-    is-preunivalent-Strict-Category x y =
-      is-emb-is-injective
-        ( is-set-type-subtype
-          ( is-iso-prop-Precategory (precategory-Strict-Category C))
-          ( is-set-hom-Strict-Category C x y))
-        ( λ _ → eq-is-prop (is-set-obj-Strict-Category C x y))
+    is-preunivalent-Strict-Category x =
+      is-set-Σ
+        ( is-set-obj-Strict-Category C)
+        ( λ y → is-set-iso-Precategory (precategory-Strict-Category C) {x} {y})
 
   preunivalent-category-Strict-Category : Preunivalent-Category l1 l2
   pr1 preunivalent-category-Strict-Category = precategory-Strict-Category C

src/foundation-core/equality-dependent-pair-types.lagda.md

@@ -168,6 +168,17 @@ module _
   ap-pr1-eq-pair-Σ refl refl = refl
 ```
 
+### Transport in `B` along the first projection of an identification in `Σ A B`
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  tr-eq-Σ : {x y : Σ A B} (p : x ＝ y) → tr B (ap pr1 p) (pr2 x) ＝ pr2 y
+  tr-eq-Σ refl = refl
+```
+
 ## See also
 
 - Equality proofs in cartesian product types are characterized in

src/foundation-core/injective-maps.lagda.md

@@ -90,6 +90,9 @@ module _
     is-injective h → is-injective g → is-injective (g ∘ h)
   is-injective-comp is-inj-h is-inj-g = is-inj-h ∘ is-inj-g
 
+  comp-injection : injection B C → injection A B → injection A C
+  comp-injection (g , G) (h , H) = (g ∘ h , is-injective-comp H G)
+
   is-injective-left-map-triangle :
     (f : A → C) (g : B → C) (h : A → B) → f ~ (g ∘ h) →
     is-injective h → is-injective g → is-injective f
@@ -111,6 +114,9 @@ module _
   is-injective-equiv : (e : A ≃ B) → is-injective (map-equiv e)
   is-injective-equiv e = is-injective-is-equiv (is-equiv-map-equiv e)
 
+  injection-equiv : A ≃ B → injection A B
+  injection-equiv e = (map-equiv e , is-injective-equiv e)
+
 abstract
   is-injective-map-inv-equiv :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →

src/foundation.lagda.md

@@ -392,9 +392,11 @@ open import foundation.standard-ternary-pullbacks public
 open import foundation.strict-symmetrization-binary-relations public
 open import foundation.strictly-involutive-identity-types public
 open import foundation.strictly-right-unital-concatenation-identifications public
+open import foundation.strong-preunivalence public
 open import foundation.strongly-extensional-maps public
 open import foundation.structure public
 open import foundation.structure-identity-principle public
+open import foundation.structured-equality-duality public
 open import foundation.structured-type-duality public
 open import foundation.subsingleton-induction public
 open import foundation.subterminal-types public

src/foundation/functoriality-dependent-function-types.lagda.md

@@ -121,7 +121,7 @@ id-map-equiv-Π B h = eq-htpy (compute-map-equiv-Π B id-equiv (λ _ → id-equi
 
 ```agda
 module _
-  { l1 l2 l3 : Level} {A : UU l1}
+  {l1 l2 l3 : Level} {A : UU l1}
   where
 
   equiv-htpy-map-Π-fam-equiv :
@@ -133,35 +133,32 @@ module _
       ( λ a → equiv-ap (e a) (f a) (g a))
 ```
 
-### Truncated families of maps induce truncated maps on dependent function types
+### Families of truncated maps induce truncated maps on dependent function types
 
 ```agda
-abstract
-  is-trunc-map-map-Π :
-    (k : 𝕋) {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-    (f : (i : I) → A i → B i) →
-    ((i : I) → is-trunc-map k (f i)) → is-trunc-map k (map-Π f)
-  is-trunc-map-map-Π k {I = I} f H h =
-    is-trunc-equiv' k
-      ( (i : I) → fiber (f i) (h i))
-      ( compute-fiber-map-Π f h)
-      ( is-trunc-Π k (λ i → H i (h i)))
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
+  where
 
-abstract
-  is-emb-map-Π :
-    {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-    {f : (i : I) → A i → B i} →
-    ((i : I) → is-emb (f i)) → is-emb (map-Π f)
-  is-emb-map-Π {f = f} H =
-    is-emb-is-prop-map
-      ( is-trunc-map-map-Π neg-one-𝕋 f
-        ( λ i → is-prop-map-is-emb (H i)))
-
-emb-Π :
-  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3} →
-  ((i : I) → A i ↪ B i) → ((i : I) → A i) ↪ ((i : I) → B i)
-pr1 (emb-Π f) = map-Π (λ i → map-emb (f i))
-pr2 (emb-Π f) = is-emb-map-Π (λ i → is-emb-map-emb (f i))
+  abstract
+    is-trunc-map-map-Π :
+      (k : 𝕋) (f : (i : I) → A i → B i) →
+      ((i : I) → is-trunc-map k (f i)) → is-trunc-map k (map-Π f)
+    is-trunc-map-map-Π k f H h =
+      is-trunc-equiv' k
+        ( (i : I) → fiber (f i) (h i))
+        ( compute-fiber-map-Π f h)
+        ( is-trunc-Π k (λ i → H i (h i)))
+
+  abstract
+    is-emb-map-Π :
+      {f : (i : I) → A i → B i} → ((i : I) → is-emb (f i)) → is-emb (map-Π f)
+    is-emb-map-Π {f} H =
+      is-emb-is-prop-map
+        ( is-trunc-map-map-Π neg-one-𝕋 f (λ i → is-prop-map-is-emb (H i)))
+
+  emb-Π : ((i : I) → A i ↪ B i) → ((i : I) → A i) ↪ ((i : I) → B i)
+  emb-Π f = (map-Π (map-emb ∘ f) , is-emb-map-Π (is-emb-map-emb ∘ f))
 ```
 
 ### A family of truncated maps over any map induces a truncated map on dependent function types