Some extensions of the fundamental theorem of identity types

src/foundation.lagda.md

@@ -211,6 +211,7 @@ open import foundation.functoriality-set-quotients public
 open import foundation.functoriality-set-truncation public
 open import foundation.functoriality-truncation public
 open import foundation.fundamental-theorem-of-identity-types public
+open import foundation.fundamental-theorem-of-identity-types-structures public
 open import foundation.global-choice public
 open import foundation.global-subuniverses public
 open import foundation.globular-type-of-dependent-functions public

src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md

@@ -0,0 +1,121 @@
+# The fundamental theorem of identity types for structures
+
+```agda
+module foundation.fundamental-theorem-of-identity-types-structures where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.maps-in-subuniverses
+open import foundation.separated-types-subuniverses
+open import foundation.subuniverses
+open import foundation.universe-levels
+
+open import foundation-core.contractible-types
+open import foundation-core.equivalences
+open import foundation-core.families-of-equivalences
+open import foundation-core.fibers-of-maps
+open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-pair-types
+open import foundation-core.homotopies
+open import foundation-core.retractions
+open import foundation-core.retracts-of-types
+open import foundation-core.sections
+open import foundation-core.torsorial-type-families
+```
+
+</details>
+
+## Idea
+
+> TODO
+
+## Theorem
+
+### The unbased fundamental theorem of identity types for structures
+
+Given a structure `𝒫` on types, then the following are logically equivalent:
+
+1. Every unbased map out of the identity types of `A` into the type family
+   `B : A → 𝒰` is `𝒫`-structured.
+2. The identity types of `Σ A B` are `𝒫`-structured.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {𝒫 : UU (l1 ⊔ l2) → UU l3}
+  (tr-𝒫 : {X Y : UU (l1 ⊔ l2)} → X ≃ Y → 𝒫 X → 𝒫 Y)
+  {A : UU l1} {B : A → UU l2}
+  where
+
+  forward-implication-fundamental-theorem-unbased-id-structure :
+    ( (x : A) (f : (y : A) → (x ＝ y) → B y)
+      (y : A) (b : B y) → 𝒫 (fiber (f y) b)) →
+    (p q : Σ A B) → 𝒫 (p ＝ q)
+  forward-implication-fundamental-theorem-unbased-id-structure
+    K (x , b) (x' , b') =
+    tr-𝒫
+      ( compute-fiber-map-out-of-identity-type (ind-Id x (λ u _ → B u) b) x' b')
+      ( K x (ind-Id x (λ u _ → B u) b) x' b')
+
+  backward-implication-fundamental-theorem-unbased-id-structure :
+    ( (p q : Σ A B) → 𝒫 (p ＝ q)) →
+    ( (x : A) (f : (y : A) → (x ＝ y) → B y)
+      (y : A) (b : B y) → 𝒫 (fiber (f y) b))
+  backward-implication-fundamental-theorem-unbased-id-structure K x f y b =
+    tr-𝒫
+      ( inv-compute-fiber-map-out-of-identity-type f y b)
+      ( K (x , f x refl) (y , b))
+
+  fundamental-theorem-unbased-id-structure :
+    ( (x : A) (f : (y : A) → (x ＝ y) → B y)
+      (y : A) (b : B y) → 𝒫 (fiber (f y) b)) ↔
+    ( (p q : Σ A B) → 𝒫 (p ＝ q))
+  fundamental-theorem-unbased-id-structure =
+    ( forward-implication-fundamental-theorem-unbased-id-structure ,
+      backward-implication-fundamental-theorem-unbased-id-structure)
+```
+
+### The unbased fundamental theorem of identity types for subuniverses
+
+Given a subuniverse `𝒫` then the following are logically equivalent:
+
+1. Every unbased map out of the identity types of `A` into the type family
+   `B : A → 𝒰` is in `𝒫`.
+2. The dependent sum `Σ A B` is `𝒫`-separated.
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒫 : subuniverse (l1 ⊔ l2) l3)
+  {A : UU l1} {B : A → UU l2}
+  where
+
+  abstract
+    forward-implication-fundamental-theorem-unbased-id-subuniverse :
+      ( (x : A) (f : (y : A) → (x ＝ y) → B y)
+        (y : A) → is-in-subuniverse-map 𝒫 (f y)) →
+      is-separated 𝒫 (Σ A B)
+    forward-implication-fundamental-theorem-unbased-id-subuniverse =
+      forward-implication-fundamental-theorem-unbased-id-structure
+        ( is-in-subuniverse-equiv 𝒫)
+
+  abstract
+    backward-implication-fundamental-theorem-unbased-id-subuniverse :
+      is-separated 𝒫 (Σ A B) →
+      ( (x : A) (f : (y : A) → (x ＝ y) → B y)
+        (y : A) → is-in-subuniverse-map 𝒫 (f y))
+    backward-implication-fundamental-theorem-unbased-id-subuniverse =
+      backward-implication-fundamental-theorem-unbased-id-structure
+        ( is-in-subuniverse-equiv 𝒫)
+
+  abstract
+    fundamental-theorem-unbased-id-subuniverse :
+      ( (x : A) (f : (y : A) → (x ＝ y) → B y)
+        (y : A) → is-in-subuniverse-map 𝒫 (f y)) ↔
+      is-separated 𝒫 (Σ A B)
+    fundamental-theorem-unbased-id-subuniverse =
+      fundamental-theorem-unbased-id-structure (is-in-subuniverse-equiv 𝒫)
+```

src/foundation/identity-types.lagda.md

@@ -318,21 +318,21 @@ module _
 
 ### Computation of fibers of families of maps out of the identity type
 
-We show that `fiber (f x) y ≃ ((* , f * refl) ＝ (x , y))` for every `x : A` and
-`y : B x`.
+Given a map `f : (x : A) → (* ＝ x) → B x`, we show that
+`fiber (f x) y ≃ ((* , f * refl) ＝ (x , y))` for every `x : A` and `y : B x`.
 
 ```agda
 module _
   {l1 l2 : Level} {A : UU l1} {a : A} {B : A → UU l2}
-  (f : (x : A) → (a ＝ x) → B x) (x : A) (y : B x)
+  (f : (x : A) → (a ＝ x) → B x) (x : A) (x' : B x)
   where
 
   map-compute-fiber-map-out-of-identity-type :
-    fiber (f x) y → ((a , f a refl) ＝ (x , y))
+    fiber (f x) x' → ((a , f a refl) ＝ (x , x'))
   map-compute-fiber-map-out-of-identity-type (refl , refl) = refl
 
   map-inv-compute-fiber-map-out-of-identity-type :
-    ((a , f a refl) ＝ (x , y)) → fiber (f x) y
+    ((a , f a refl) ＝ (x , x')) → fiber (f x) x'
   map-inv-compute-fiber-map-out-of-identity-type refl =
     refl , refl
 
@@ -355,10 +355,70 @@ module _
       is-section-map-inv-compute-fiber-map-out-of-identity-type
       is-retraction-map-inv-compute-fiber-map-out-of-identity-type
 
+  is-equiv-map-inv-compute-fiber-map-out-of-identity-type :
+    is-equiv map-inv-compute-fiber-map-out-of-identity-type
+  is-equiv-map-inv-compute-fiber-map-out-of-identity-type =
+    is-equiv-is-invertible
+      map-compute-fiber-map-out-of-identity-type
+      is-retraction-map-inv-compute-fiber-map-out-of-identity-type
+      is-section-map-inv-compute-fiber-map-out-of-identity-type
+
   compute-fiber-map-out-of-identity-type :
-    fiber (f x) y ≃ ((a , f a refl) ＝ (x , y))
-  pr1 compute-fiber-map-out-of-identity-type =
-    map-compute-fiber-map-out-of-identity-type
-  pr2 compute-fiber-map-out-of-identity-type =
-    is-equiv-map-compute-fiber-map-out-of-identity-type
+    fiber (f x) x' ≃ ((a , f a refl) ＝ (x , x'))
+  compute-fiber-map-out-of-identity-type =
+    ( map-compute-fiber-map-out-of-identity-type ,
+      is-equiv-map-compute-fiber-map-out-of-identity-type)
+
+  inv-compute-fiber-map-out-of-identity-type :
+    ((a , f a refl) ＝ (x , x')) ≃ fiber (f x) x'
+  inv-compute-fiber-map-out-of-identity-type =
+    ( map-inv-compute-fiber-map-out-of-identity-type ,
+      is-equiv-map-inv-compute-fiber-map-out-of-identity-type)
+```
+
+### Computation of fibers of families of unbased maps out of the identity type
+
+Given a map `f : (x y : A) → (x ＝ y) → B x y`, we show that
+`fiber (f x y) b ≃ ((x , f x x refl) ＝ (y , b))` for every `x y : A` and
+`b : B x y`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → A → UU l2}
+  (f : (x y : A) → x ＝ y → B x y) (x y : A) (b : B x y)
+  where
+
+  map-compute-fiber-unbased-map-out-of-identity-type :
+    fiber (f x y) b → (x , f x x refl) ＝ (y , b)
+  map-compute-fiber-unbased-map-out-of-identity-type (refl , refl) = refl
+
+  map-inv-compute-fiber-unbased-map-out-of-identity-type :
+    (x , f x x refl) ＝ (y , b) → fiber (f x y) b
+  map-inv-compute-fiber-unbased-map-out-of-identity-type refl = (refl , refl)
+
+  is-section-map-inv-compute-fiber-unbased-map-out-of-identity-type :
+    map-compute-fiber-unbased-map-out-of-identity-type ∘
+    map-inv-compute-fiber-unbased-map-out-of-identity-type ~ id
+  is-section-map-inv-compute-fiber-unbased-map-out-of-identity-type refl = refl
+
+  is-retraction-map-inv-compute-fiber-unbased-map-out-of-identity-type :
+    map-inv-compute-fiber-unbased-map-out-of-identity-type ∘
+    map-compute-fiber-unbased-map-out-of-identity-type ~ id
+  is-retraction-map-inv-compute-fiber-unbased-map-out-of-identity-type
+    ( refl , refl) =
+    refl
+
+  is-equiv-map-compute-fiber-unbased-map-out-of-identity-type :
+    is-equiv map-compute-fiber-unbased-map-out-of-identity-type
+  is-equiv-map-compute-fiber-unbased-map-out-of-identity-type =
+    is-equiv-is-invertible
+      map-inv-compute-fiber-unbased-map-out-of-identity-type
+      is-section-map-inv-compute-fiber-unbased-map-out-of-identity-type
+      is-retraction-map-inv-compute-fiber-unbased-map-out-of-identity-type
+
+  compute-fiber-unbased-map-out-of-identity-type :
+    fiber (f x y) b ≃ ((x , f x x refl) ＝ (y , b))
+  compute-fiber-unbased-map-out-of-identity-type =
+    ( map-compute-fiber-unbased-map-out-of-identity-type ,
+      is-equiv-map-compute-fiber-unbased-map-out-of-identity-type)
 ```

src/foundation/maps-in-subuniverses.lagda.md

@@ -7,6 +7,7 @@ module foundation.maps-in-subuniverses where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.homotopies
 open import foundation.subuniverses
 open import foundation.universe-levels
 
@@ -33,6 +34,22 @@ is-in-subuniverse-map :
 is-in-subuniverse-map P {A} {B} f = (b : B) → is-in-subuniverse P (fiber f b)
 ```
 
+## Properties
+
+### Subuniverses are closed under homotopies of maps
+
+```agda
+module _
+  {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) {A : UU l1} {B : UU l2}
+  {f g : A → B}
+  where
+
+  is-in-subuniverse-map-htpy :
+    f ~ g → is-in-subuniverse-map P f → is-in-subuniverse-map P g
+  is-in-subuniverse-map-htpy H F y =
+    is-in-subuniverse-equiv' P (equiv-fiber-htpy H y) (F y)
+```
+
 ## See also
 
 - [Maps in global subuniverses](foundation.maps-in-global-subuniverses.md)

src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md

@@ -82,6 +82,8 @@ agda-unimath.
 
 ## Theorem
 
+### The based extended fundamental theorem of identity types
+
 ```agda
 module _
   {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3)
@@ -96,15 +98,15 @@ module _
     forward-implication-extended-fundamental-theorem-id H K (x , y) (x' , y') =
       apply-universal-property-trunc-Prop
         ( mere-eq-is-0-connected H a x)
-        ( P _)
+        ( P ((x , y) ＝ (x' , y')))
         ( λ where
           refl →
             is-in-subuniverse-equiv P
               ( compute-fiber-map-out-of-identity-type
-                ( ind-Id a (λ u v → B u) y)
+                ( ind-Id a (λ u _ → B u) y)
                 ( x')
                 ( y'))
-              ( K (ind-Id a (λ u v → B u) y) x' y'))
+              ( K (ind-Id a (λ u _ → B u) y) x' y'))
 
   abstract
     backward-implication-extended-fundamental-theorem-id :

src/foundation/univalent-type-families.lagda.md

@@ -43,7 +43,8 @@ map
 is an [equivalence](foundation-core.equivalences.md) for every `x y : A`. By
 [the univalence axiom](foundation-core.univalence.md), this is equivalent to the
 type family `B` being an [embedding](foundation-core.embeddings.md) considered
-as a map.
+as a map. In other words, that `A` is a
+[subuniverse](foundation.subuniverses.md).
 
 ## Definition