From bc13587570ad557c730f0b3a260422aac4159af0 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 27 Jan 2025 20:00:11 +0100 Subject: [PATCH 01/23] unbased extended fundamental theorem of identity types --- src/foundation/identity-types.lagda.md | 54 +++++++++++++++-- src/foundation/maps-in-subuniverses.lagda.md | 17 ++++++ ...amental-theorem-of-identity-types.lagda.md | 58 ++++++++++++++++++- .../univalent-type-families.lagda.md | 3 +- 4 files changed, 124 insertions(+), 8 deletions(-) diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md index 8bbd6bea4c..3065d76f51 100644 --- a/src/foundation/identity-types.lagda.md +++ b/src/foundation/identity-types.lagda.md @@ -324,15 +324,15 @@ We show that `fiber (f x) y ≃ ((* , f * refl) ＝ (x , y))` for every `x : A` ```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 @@ -356,9 +356,55 @@ module _ is-retraction-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)) + fiber (f x) x' ≃ ((a , f a refl) ＝ (x , x')) 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 ``` + +### Computation of fibers of families of unbased maps out of the identity type + +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) +``` diff --git a/src/foundation/maps-in-subuniverses.lagda.md b/src/foundation/maps-in-subuniverses.lagda.md index 54aab010e1..52c43cb7cc 100644 --- a/src/foundation/maps-in-subuniverses.lagda.md +++ b/src/foundation/maps-in-subuniverses.lagda.md @@ -7,6 +7,7 @@ module foundation.maps-in-subuniverses where
Imports ```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) diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index 14db96e387..2e87a332a7 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -25,6 +25,7 @@ open import foundation.identity-types open import foundation.inhabited-types open import foundation.logical-equivalences open import foundation.maps-in-subuniverses +open import foundation.mere-equality open import foundation.propositional-truncations open import foundation.separated-types-subuniverses open import foundation.subuniverses @@ -82,6 +83,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 +99,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 x (λ 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 : @@ -126,6 +129,55 @@ module _ backward-implication-extended-fundamental-theorem-id ``` +### The unbased extended fundamental theorem of identity types + +```agda +module _ + {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) + {A : UU l1} {B : A → UU l2} + where + + abstract + forward-implication-extended-fundamental-theorem-unbased-id : + ( (x y : A) → mere-eq x y) → + ( (x : A) (f : (y : A) → (x ＝ y) → B y) + (y : A) → is-in-subuniverse-map P (f y)) → + is-separated P (Σ A B) + forward-implication-extended-fundamental-theorem-unbased-id + H K (x , b) (x' , b') = + apply-universal-property-trunc-Prop + ( H x x') + ( P ((x , b) ＝ (x' , b'))) + ( λ where + refl → + is-in-subuniverse-equiv P + ( 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')) + + abstract + backward-implication-extended-fundamental-theorem-unbased-id : + is-separated P (Σ A B) → + ( (x : A) (f : (y : A) → (x ＝ y) → B y) + (y : A) → is-in-subuniverse-map P (f y)) + backward-implication-extended-fundamental-theorem-unbased-id K x f y b = + is-in-subuniverse-equiv' P + ( compute-fiber-map-out-of-identity-type f y b) + ( K (x , f x refl) (y , b)) + + abstract + extended-fundamental-theorem-unbased-id : + ( (x y : A) → mere-eq x y) → + ( (x : A) (f : (y : A) → (x ＝ y) → B y) + (y : A) → is-in-subuniverse-map P (f y)) ↔ + is-separated P (Σ A B) + extended-fundamental-theorem-unbased-id H = + ( forward-implication-extended-fundamental-theorem-unbased-id H , + backward-implication-extended-fundamental-theorem-unbased-id) +``` + ## Corollaries ### Characterizing families of surjective maps out of identity types diff --git a/src/foundation/univalent-type-families.lagda.md b/src/foundation/univalent-type-families.lagda.md index 129dfaf7be..9a7c109a9a 100644 --- a/src/foundation/univalent-type-families.lagda.md +++ b/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 From 72247349acd4e909a0ab2ca65daadc58b8b399a7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 27 Jan 2025 20:11:03 +0100 Subject: [PATCH 02/23] some prose --- src/foundation/identity-types.lagda.md | 9 +++++---- ...ension-fundamental-theorem-of-identity-types.lagda.md | 4 ++++ 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md index 3065d76f51..b155ca4b20 100644 --- a/src/foundation/identity-types.lagda.md +++ b/src/foundation/identity-types.lagda.md @@ -318,8 +318,8 @@ 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 _ @@ -365,8 +365,9 @@ module _ ### Computation of fibers of families of unbased maps out of the identity type -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`. +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 _ diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index 2e87a332a7..fa76c2718b 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -131,6 +131,10 @@ module _ ### The unbased extended fundamental theorem of identity types +The following is an unbased version of the extended fundamental theorem of +identity types. For this formulation of the theorem we do not need to assume +that `A` is inhabited. + ```agda module _ {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) From 8cfd888d70359f73be0f8f4485f9f39a69cb3d7a Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 27 Jan 2025 20:15:42 +0100 Subject: [PATCH 03/23] revert two symbols --- ...urg-extension-fundamental-theorem-of-identity-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index fa76c2718b..817bada235 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -104,7 +104,7 @@ module _ refl → is-in-subuniverse-equiv P ( compute-fiber-map-out-of-identity-type - ( ind-Id x (λ u _ → B u) y) + ( ind-Id a (λ u _ → B u) y) ( x') ( y')) ( K (ind-Id a (λ u _ → B u) y) x' y')) From 92b0358d7512cb3e0ee0bebae5e7bf371ee54dc6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 27 Jan 2025 20:59:57 +0100 Subject: [PATCH 04/23] fundamental theorem of identity types for structures and subuniverses --- src/foundation.lagda.md | 1 + ...orem-of-identity-types-structures.lagda.md | 109 ++++++++++++++++++ src/foundation/identity-types.lagda.md | 21 +++- ...amental-theorem-of-identity-types.lagda.md | 54 --------- 4 files changed, 127 insertions(+), 58 deletions(-) create mode 100644 src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 4e72fe1c04..c4b3747dbe 100644 --- a/src/foundation.lagda.md +++ b/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 diff --git a/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md b/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md new file mode 100644 index 0000000000..ca31351f16 --- /dev/null +++ b/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md @@ -0,0 +1,109 @@ +# The fundamental theorem of identity types for structures + +```agda +module foundation.fundamental-theorem-of-identity-types-structures where +``` + +
Imports + +```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 +``` + +
+ +## Idea + +> TODO + +## Theorem + +### The unbased fundamental theorem of identity types for structures + +```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 + +```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 𝒫) +``` diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md index b155ca4b20..98e45b05e8 100644 --- a/src/foundation/identity-types.lagda.md +++ b/src/foundation/identity-types.lagda.md @@ -355,12 +355,25 @@ 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) x' ≃ ((a , f a refl) ＝ (x , x')) - 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 + 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 diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index 817bada235..e208bcd951 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -25,7 +25,6 @@ open import foundation.identity-types open import foundation.inhabited-types open import foundation.logical-equivalences open import foundation.maps-in-subuniverses -open import foundation.mere-equality open import foundation.propositional-truncations open import foundation.separated-types-subuniverses open import foundation.subuniverses @@ -129,59 +128,6 @@ module _ backward-implication-extended-fundamental-theorem-id ``` -### The unbased extended fundamental theorem of identity types - -The following is an unbased version of the extended fundamental theorem of -identity types. For this formulation of the theorem we do not need to assume -that `A` is inhabited. - -```agda -module _ - {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) - {A : UU l1} {B : A → UU l2} - where - - abstract - forward-implication-extended-fundamental-theorem-unbased-id : - ( (x y : A) → mere-eq x y) → - ( (x : A) (f : (y : A) → (x ＝ y) → B y) - (y : A) → is-in-subuniverse-map P (f y)) → - is-separated P (Σ A B) - forward-implication-extended-fundamental-theorem-unbased-id - H K (x , b) (x' , b') = - apply-universal-property-trunc-Prop - ( H x x') - ( P ((x , b) ＝ (x' , b'))) - ( λ where - refl → - is-in-subuniverse-equiv P - ( 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')) - - abstract - backward-implication-extended-fundamental-theorem-unbased-id : - is-separated P (Σ A B) → - ( (x : A) (f : (y : A) → (x ＝ y) → B y) - (y : A) → is-in-subuniverse-map P (f y)) - backward-implication-extended-fundamental-theorem-unbased-id K x f y b = - is-in-subuniverse-equiv' P - ( compute-fiber-map-out-of-identity-type f y b) - ( K (x , f x refl) (y , b)) - - abstract - extended-fundamental-theorem-unbased-id : - ( (x y : A) → mere-eq x y) → - ( (x : A) (f : (y : A) → (x ＝ y) → B y) - (y : A) → is-in-subuniverse-map P (f y)) ↔ - is-separated P (Σ A B) - extended-fundamental-theorem-unbased-id H = - ( forward-implication-extended-fundamental-theorem-unbased-id H , - backward-implication-extended-fundamental-theorem-unbased-id) -``` - ## Corollaries ### Characterizing families of surjective maps out of identity types From 8844fcb5df7464e242f910347edea4a66e51c023 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 27 Jan 2025 21:10:04 +0100 Subject: [PATCH 05/23] mild explanation --- ...tal-theorem-of-identity-types-structures.lagda.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md b/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md index ca31351f16..f608a89192 100644 --- a/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md +++ b/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md @@ -38,6 +38,12 @@ open import foundation-core.torsorial-type-families ### 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} @@ -75,6 +81,12 @@ module _ ### 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) From a58c9ccb5c7ca64da570aec24a62bd14b2f737a0 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 12:20:08 +0100 Subject: [PATCH 06/23] the unbased extended fundamental theorem proper --- ...amental-theorem-of-identity-types.lagda.md | 51 ++++++++++++++++++- 1 file changed, 50 insertions(+), 1 deletion(-) diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index e208bcd951..a284d8f3ea 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -25,6 +25,7 @@ open import foundation.identity-types open import foundation.inhabited-types open import foundation.logical-equivalences open import foundation.maps-in-subuniverses +open import foundation.mere-equality open import foundation.propositional-truncations open import foundation.separated-types-subuniverses open import foundation.subuniverses @@ -82,7 +83,7 @@ agda-unimath. ## Theorem -### The based extended fundamental theorem of identity types +### The extended fundamental theorem of identity types ```agda module _ @@ -128,6 +129,54 @@ module _ backward-implication-extended-fundamental-theorem-id ``` +### The unbased extended fundamental theorem of identity types + +```agda +module _ + {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) + {A : UU l1} (a : A) {B : A → A → UU l2} + where + + abstract + forward-implication-extended-fundamental-theorem-unbased-id : + ( (x y : A) → mere-eq x y) → + ( (x : A) (f : (y : A) → (x ＝ y) → B x y) + (y : A) → is-in-subuniverse-map P (f y)) → + ( (x : A) → is-separated P (Σ A (B x))) + forward-implication-extended-fundamental-theorem-unbased-id + H K x (y , b) (y' , b') = + apply-universal-property-trunc-Prop + ( H x y) + ( P ((y , b) ＝ (y' , b'))) + ( λ where + refl → + is-in-subuniverse-equiv P + ( compute-fiber-map-out-of-identity-type + ( ind-Id x (λ u _ → B x u) b) + ( y') + ( b')) + ( K x (ind-Id x (λ u _ → B x u) b) y' b')) + + backward-implication-extended-fundamental-theorem-unbased-id : + ( (x : A) → is-separated P (Σ A (B x))) → + ( (x : A) (f : (y : A) → (x ＝ y) → B x y) + (y : A) → is-in-subuniverse-map P (f y)) + backward-implication-extended-fundamental-theorem-unbased-id K x f y b = + is-in-subuniverse-equiv' P + ( compute-fiber-map-out-of-identity-type f y b) + ( K x (x , f x refl) (y , b)) + + abstract + extended-fundamental-theorem-unbased-id : + ( (x y : A) → mere-eq x y) → + ( (x : A) (f : (y : A) → (x ＝ y) → B x y) + (y : A) → is-in-subuniverse-map P (f y)) ↔ + ( (x : A) → is-separated P (Σ A (B x))) + extended-fundamental-theorem-unbased-id H = + ( forward-implication-extended-fundamental-theorem-unbased-id H , + backward-implication-extended-fundamental-theorem-unbased-id) +``` + ## Corollaries ### Characterizing families of surjective maps out of identity types From 82bbf22ce19e5b992cc0740c7ada927011703155 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 13:08:19 +0100 Subject: [PATCH 07/23] explanation extended fundamental theorem --- ...on-fundamental-theorem-of-identity-types.lagda.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index a284d8f3ea..7cbb33831f 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -131,10 +131,20 @@ module _ ### The unbased extended fundamental theorem of identity types +We can give a similar characterization for a binary family of types +`B : A → A → 𝒰` over a not necessarily pointed or inhabited type `A` whose +elements are all merely equal. In other words, `A` is any π₀-trivial type. The +characterization asserts that the following are equivalent: + +1. For every `x : A` and every family of maps out of the identity types + `f : (y : A) → (x ＝ y) → B x y`, then for every `y : A` the `f y` is a + `P`-map. +2. For every `x : A` the type `Σ A (B x)` is `P`-separated. + ```agda module _ {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) - {A : UU l1} (a : A) {B : A → A → UU l2} + {A : UU l1} {B : A → A → UU l2} where abstract From 3b7c9dcc37c67c6aa6bb3ac39a244018bb623dee Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 15:02:17 +0100 Subject: [PATCH 08/23] universal property of identity types follows from injectivity of `equiv-eq` --- .../equality-dependent-pair-types.lagda.md | 11 ++ src/foundation-core/injective-maps.lagda.md | 6 + ...oriality-dependent-function-types.lagda.md | 51 ++++---- src/foundation/injective-maps.lagda.md | 48 +++++++- ...universal-property-identity-types.lagda.md | 111 +++++++++++++----- 5 files changed, 165 insertions(+), 62 deletions(-) diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md index 9dacb2ce72..5668a7cc6e 100644 --- a/src/foundation-core/equality-dependent-pair-types.lagda.md +++ b/src/foundation-core/equality-dependent-pair-types.lagda.md @@ -168,6 +168,17 @@ module _ ap-pr1-eq-pair-Σ refl refl = refl ``` +### Transporting 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 diff --git a/src/foundation-core/injective-maps.lagda.md b/src/foundation-core/injective-maps.lagda.md index bf6bc84c72..72003be269 100644 --- a/src/foundation-core/injective-maps.lagda.md +++ b/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) → diff --git a/src/foundation/functoriality-dependent-function-types.lagda.md b/src/foundation/functoriality-dependent-function-types.lagda.md index 5993ac6c2a..9fc8e6c98c 100644 --- a/src/foundation/functoriality-dependent-function-types.lagda.md +++ b/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 diff --git a/src/foundation/injective-maps.lagda.md b/src/foundation/injective-maps.lagda.md index 8114a8e0f3..8ab3913353 100644 --- a/src/foundation/injective-maps.lagda.md +++ b/src/foundation/injective-maps.lagda.md @@ -9,12 +9,18 @@ open import foundation-core.injective-maps public
Imports ```agda +open import foundation.action-on-identifications-dependent-functions +open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.logical-equivalences +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation-core.embeddings open import foundation-core.empty-types +open import foundation-core.equality-dependent-pair-types +open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.negation @@ -102,15 +108,51 @@ module _ is-set A → (f : A → B) → is-prop (is-injective f) is-prop-is-injective H f = is-prop-implicit-Π - ( λ x → - is-prop-implicit-Π - ( λ y → is-prop-function-type (H x y))) + ( λ x → is-prop-implicit-Π (λ y → is-prop-function-type (H x y))) is-injective-Prop : is-set A → (A → B) → Prop (l1 ⊔ l2) pr1 (is-injective-Prop H f) = is-injective f pr2 (is-injective-Prop H f) = is-prop-is-injective H f ``` +### The map on total spaces induced by a family of injective maps is an injective map + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + where + is-injective-tot : + {f : (x : A) → B x → C x} → + ((x : A) → is-injective (f x)) → + is-injective (tot f) + is-injective-tot {f} H {x} {y} p = + eq-pair-Σ + ( ap pr1 p) + ( H (pr1 y) (preserves-tr f (ap pr1 p) (pr2 x) ∙ tr-eq-Σ p)) + + injection-tot : ((x : A) → injection (B x) (C x)) → injection (Σ A B) (Σ A C) + injection-tot f = (tot (pr1 ∘ f) , is-injective-tot (pr2 ∘ f)) +``` + +### Families of injective maps induce injective maps on dependent function types + +```agda +module _ + {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3} + where + + abstract + is-injective-map-Π : + {f : (i : I) → A i → B i} → + ((i : I) → is-injective (f i)) → is-injective (map-Π f) + is-injective-map-Π {f = f} H {x} {y} p = eq-htpy (λ i → H i (htpy-eq p i)) + + injection-Π : + ((i : I) → injection (A i) (B i)) → + injection ((i : I) → A i) ((i : I) → B i) + injection-Π f = (map-Π (pr1 ∘ f) , is-injective-map-Π (pr2 ∘ f)) +``` + ## See also - [Embeddings](foundation-core.embeddings.md) diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md index 678401d075..eafff48723 100644 --- a/src/foundation/universal-property-identity-types.lagda.md +++ b/src/foundation/universal-property-identity-types.lagda.md @@ -17,6 +17,7 @@ open import foundation.function-extensionality open import foundation.functoriality-dependent-function-types open import foundation.fundamental-theorem-of-identity-types open import foundation.identity-types +open import foundation.injective-maps open import foundation.preunivalence open import foundation.univalence open import foundation.universe-levels @@ -28,7 +29,6 @@ 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.injective-maps open import foundation-core.propositional-maps open import foundation-core.propositions open import foundation-core.torsorial-type-families @@ -38,9 +38,9 @@ open import foundation-core.torsorial-type-families ## Idea -The **universal property of identity types** characterizes families of maps out -of the [identity type](foundation-core.identity-types.md). This universal -property is also known as the **type theoretic Yoneda lemma**. +The {{#concept "universal property of identity types"}} characterizes families +of maps out of the [identity type](foundation-core.identity-types.md). This +universal property is also known as the **type theoretic Yoneda lemma**. ## Theorem @@ -113,40 +113,92 @@ module _ ### `Id : A → (A → 𝒰)` is an embedding -We first show that [the preunivalence axiom](foundation.preunivalence.md) -implies that the map `Id : A → (A → 𝒰)` is an +We first show that [injectivity](foundation-core.injective-maps.md) of the map + +```text + equiv-eq : {X Y : 𝓤} → (X ＝ Y) → (X ≃ Y) +``` + +for the identity types of `A` implies that the map `Id : A → (A → 𝒰)` is an [embedding](foundation.embeddings.md). Since the -[univalence axiom](foundation.univalence.md) implies preunivalence, it follows -that `Id : A → (A → 𝒰)` is an embedding under the postulates of agda-unimath. +[univalence axiom](foundation.univalence.md) implies +[the preunivalence axiom](foundation.preunivalence.md) implies injectivity of +`equiv-eq`, it follows that `Id : A → (A → 𝒰)` is an embedding under the +postulates of agda-unimath. -#### Preunivalence implies that `Id : A → (A → 𝒰)` is an embedding +#### Injectivity of `equiv-eq` implies `Id : A → (A → 𝒰)` is an embedding -The proof that preunivalence implies that `Id : A → (A → 𝒰)` is an embedding -proceeds via the +The proof that injectivity of `equiv-eq` implies that `Id : A → (A → 𝒰)` is an +embedding proceeds via the [fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md) by showing that the [fiber](foundation.fibers-of-maps.md) of `Id` at `Id a` is [contractible](foundation.contractible-types.md) for each `a : A`. To see this, we first note that this fiber has an element `(a , refl)`. Therefore it suffices to show that this fiber is a proposition. We do this by constructing an -embedding +injection ```text - fiber Id (Id a) ↪ Σ A (Id a). + fiber Id (Id a) ↣ Σ A (Id a). ``` -Since the codomain of this embedding is contractible, the claim follows. The -above embedding is constructed as the composite of the following embeddings +Since the codomain of this injection is contractible, the claim follows. The +above injection is constructed as the following composite injection ```text Σ (x : A), Id x ＝ Id a - ↪ Σ (x : A), (y : A) → (x ＝ y) ＝ (a ＝ y) - ↪ Σ (x : A), (y : A) → (x ＝ y) ≃ (a ＝ y) - ↪ Σ (x : A), Σ (e : (y : A) → (x ＝ y) → (a ＝ y)), (y : A) → is-equiv (e y) - ↪ Σ (x : A), (y : A) → (x ＝ y) → (a ＝ y) - ↪ Σ (x : A), a ＝ x. + ≃ Σ (x : A), ((y : A) → (x ＝ y) ＝ (a ＝ y)) + ↣ Σ (x : A), ((y : A) → (x ＝ y) ≃ (a ＝ y)) + ↪ Σ (x : A), ((y : A) → (x ＝ y) → (a ＝ y)) + ≃ Σ (x : A), a ＝ x. ``` -In this composite, we used preunivalence at the second step. +In this composite, the injectivity of `equiv-eq` is used in the second step. + +```agda +module _ + {l : Level} (A : UU l) + (L : (a x y : A) → is-injective (equiv-eq {A = Id x y} {B = Id a y})) + where + + injection-fiber-Id-is-injective-equiv-eq-Id : + (a : A) → injection (fiber' Id (Id a)) (Σ A (Id a)) + injection-fiber-Id-is-injective-equiv-eq-Id a = + comp-injection + ( comp-injection + ( injection-equiv + ( equiv-tot + ( λ x → + ( equiv-ev-refl x) ∘e + ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a))))) + ( injection-tot + ( λ x → + comp-injection + ( injection-Π (λ y → _ , L a x y)) + ( injection-equiv equiv-funext)))) + ( injection-equiv (inv-equiv (equiv-fiber Id (Id a)))) + + is-emb-Id-is-injective-equiv-eq-Id : is-emb (Id {A = A}) + is-emb-Id-is-injective-equiv-eq-Id a = + fundamental-theorem-id + ( ( a , refl) , + ( λ _ → + pr2 + ( injection-fiber-Id-is-injective-equiv-eq-Id a) + ( eq-is-contr (is-torsorial-Id a)))) + ( λ _ → ap Id) +``` + +#### Preunivalence implies that `Id : A → (A → 𝒰)` is an embedding + +Assuming preunivalence, then in particular `equiv-eq` is injective and so the +previous argument applies. However, in this case we do get a slightly stronger +result, since now the fiber inclusion + +```text + fiber Id (Id a) → Σ A (Id a) +``` + +is a proper embedding. ```agda module _ @@ -154,8 +206,7 @@ module _ (L : (a x y : A) → instance-preunivalence (Id x y) (Id a y)) where - emb-fiber-Id-preunivalent-Id : - (a : A) → fiber' Id (Id a) ↪ Σ A (Id a) + emb-fiber-Id-preunivalent-Id : (a : A) → fiber' Id (Id a) ↪ Σ A (Id a) emb-fiber-Id-preunivalent-Id a = comp-emb ( comp-emb @@ -172,14 +223,9 @@ module _ ( emb-equiv (inv-equiv (equiv-fiber Id (Id a)))) is-emb-Id-preunivalent-Id : is-emb (Id {A = A}) - is-emb-Id-preunivalent-Id a = - fundamental-theorem-id - ( ( a , refl) , - ( λ _ → - is-injective-emb - ( emb-fiber-Id-preunivalent-Id a) - ( eq-is-contr (is-torsorial-Id a)))) - ( λ _ → ap Id) + is-emb-Id-preunivalent-Id = + is-emb-Id-is-injective-equiv-eq-Id A + ( λ a x y → is-injective-is-emb (L a x y)) module _ (L : preunivalence-axiom) {l : Level} (A : UU l) @@ -187,7 +233,8 @@ module _ is-emb-Id-preunivalence-axiom : is-emb (Id {A = A}) is-emb-Id-preunivalence-axiom = - is-emb-Id-preunivalent-Id A (λ a x y → L (Id x y) (Id a y)) + is-emb-Id-is-injective-equiv-eq-Id A + ( λ a x y → is-injective-is-emb (L (Id x y) (Id a y))) ``` #### `Id : A → (A → 𝒰)` is an embedding From 612d84c0ed83f95d7fe3907a1f1e6f8d0720127d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 16:17:56 +0100 Subject: [PATCH 09/23] simplify proof unbased extended fundamental theorem --- ...amental-theorem-of-identity-types.lagda.md | 52 +++++++------------ 1 file changed, 20 insertions(+), 32 deletions(-) diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index 7cbb33831f..3450987fe8 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -147,44 +147,32 @@ module _ {A : UU l1} {B : A → A → UU l2} where - abstract - forward-implication-extended-fundamental-theorem-unbased-id : - ( (x y : A) → mere-eq x y) → - ( (x : A) (f : (y : A) → (x ＝ y) → B x y) - (y : A) → is-in-subuniverse-map P (f y)) → - ( (x : A) → is-separated P (Σ A (B x))) - forward-implication-extended-fundamental-theorem-unbased-id - H K x (y , b) (y' , b') = - apply-universal-property-trunc-Prop - ( H x y) - ( P ((y , b) ＝ (y' , b'))) - ( λ where - refl → - is-in-subuniverse-equiv P - ( compute-fiber-map-out-of-identity-type - ( ind-Id x (λ u _ → B x u) b) - ( y') - ( b')) - ( K x (ind-Id x (λ u _ → B x u) b) y' b')) + forward-implication-extended-fundamental-theorem-unbased-id : + ( (x y : A) → mere-eq x y) → + ( (x : A) (f : (y : A) → (x ＝ y) → B x y) + (y : A) → is-in-subuniverse-map P (f y)) → + ( (x : A) → is-separated P (Σ A (B x))) + forward-implication-extended-fundamental-theorem-unbased-id H K x = + forward-implication-extended-fundamental-theorem-id P + ( x) + ( is-0-connected-mere-eq x (H x)) + ( K x) backward-implication-extended-fundamental-theorem-unbased-id : ( (x : A) → is-separated P (Σ A (B x))) → ( (x : A) (f : (y : A) → (x ＝ y) → B x y) (y : A) → is-in-subuniverse-map P (f y)) - backward-implication-extended-fundamental-theorem-unbased-id K x f y b = - is-in-subuniverse-equiv' P - ( compute-fiber-map-out-of-identity-type f y b) - ( K x (x , f x refl) (y , b)) + backward-implication-extended-fundamental-theorem-unbased-id K x = + backward-implication-extended-fundamental-theorem-id P x (K x) - abstract - extended-fundamental-theorem-unbased-id : - ( (x y : A) → mere-eq x y) → - ( (x : A) (f : (y : A) → (x ＝ y) → B x y) - (y : A) → is-in-subuniverse-map P (f y)) ↔ - ( (x : A) → is-separated P (Σ A (B x))) - extended-fundamental-theorem-unbased-id H = - ( forward-implication-extended-fundamental-theorem-unbased-id H , - backward-implication-extended-fundamental-theorem-unbased-id) + extended-fundamental-theorem-unbased-id : + ( (x y : A) → mere-eq x y) → + ( (x : A) (f : (y : A) → (x ＝ y) → B x y) + (y : A) → is-in-subuniverse-map P (f y)) ↔ + ( (x : A) → is-separated P (Σ A (B x))) + extended-fundamental-theorem-unbased-id H = + ( forward-implication-extended-fundamental-theorem-unbased-id H , + backward-implication-extended-fundamental-theorem-unbased-id) ``` ## Corollaries From 110829101e34602ad8487a28dc4a65d59f77c761 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 18:38:27 +0100 Subject: [PATCH 10/23] edits --- ...orem-of-identity-types-structures.lagda.md | 23 ++++++------ src/foundation/identity-types.lagda.md | 36 +++---------------- src/foundation/structure.lagda.md | 36 +++++++++++-------- 3 files changed, 36 insertions(+), 59 deletions(-) diff --git a/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md b/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md index f608a89192..a80dea8713 100644 --- a/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md +++ b/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md @@ -13,6 +13,7 @@ open import foundation.logical-equivalences open import foundation.maps-in-subuniverses open import foundation.separated-types-subuniverses open import foundation.subuniverses +open import foundation.structure open import foundation.universe-levels open import foundation-core.contractible-types @@ -38,10 +39,11 @@ open import foundation-core.torsorial-type-families ### The unbased fundamental theorem of identity types for structures -Given a structure `𝒫` on types, then the following are logically equivalent: +Given a structure `𝒫` on types that transports along equivalences, 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. +1. For every `x : A`, every family of maps map out of the identity types of `A`, + `f : (y : A) → (x ＝ y) → B y` is `𝒫`-structured. 2. The identity types of `Σ A B` are `𝒫`-structured. ```agda @@ -52,9 +54,8 @@ module _ 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) + ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) → + structure-equality 𝒫 (Σ A B) forward-implication-fundamental-theorem-unbased-id-structure K (x , b) (x' , b') = tr-𝒫 @@ -62,18 +63,16 @@ module _ ( 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)) + structure-equality 𝒫 (Σ A B) → + ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) 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)) + ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) ↔ + ( structure-equality 𝒫 (Σ A B)) fundamental-theorem-unbased-id-structure = ( forward-implication-fundamental-theorem-unbased-id-structure , backward-implication-fundamental-theorem-unbased-id-structure) diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md index 98e45b05e8..2f517ddffe 100644 --- a/src/foundation/identity-types.lagda.md +++ b/src/foundation/identity-types.lagda.md @@ -385,40 +385,12 @@ Given a map `f : (x y : A) → (x ＝ y) → B x y`, we show that ```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) + (f : (x y : A) → x ＝ y → 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 : + (x y : A) (b : B x y) → 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) + compute-fiber-unbased-map-out-of-identity-type x = + compute-fiber-map-out-of-identity-type (f x) ``` diff --git a/src/foundation/structure.lagda.md b/src/foundation/structure.lagda.md index 0aa7762c1e..6a5b9217b7 100644 --- a/src/foundation/structure.lagda.md +++ b/src/foundation/structure.lagda.md @@ -21,40 +21,46 @@ open import foundation-core.transport-along-identifications ## Idea -Given a type family `P` on the universe, a **`P`-structured type** consists of a -type `A` equipped with an element of type `P A`. +Given a type family `𝒫` on the universe, a {{#concept "`𝒫`-structured type"}} +consists of a type `A` _equipped_ with an element of type `𝒫 A`. -## Definition +## Definitions ```agda -structure : {l1 l2 : Level} (P : UU l1 → UU l2) → UU (lsuc l1 ⊔ l2) -structure {l1} P = Σ (UU l1) P +structure : {l1 l2 : Level} (𝒫 : UU l1 → UU l2) → UU (lsuc l1 ⊔ l2) +structure {l1} 𝒫 = Σ (UU l1) 𝒫 fam-structure : - {l1 l2 l3 : Level} (P : UU l1 → UU l2) (A : UU l3) → UU (lsuc l1 ⊔ l2 ⊔ l3) -fam-structure P A = A → structure P + {l1 l2 l3 : Level} (𝒫 : UU l1 → UU l2) (A : UU l3) → UU (lsuc l1 ⊔ l2 ⊔ l3) +fam-structure 𝒫 A = A → structure 𝒫 structure-map : - {l1 l2 l3 : Level} (P : UU (l1 ⊔ l2) → UU l3) {A : UU l1} {B : UU l2} + {l1 l2 l3 : Level} (𝒫 : UU (l1 ⊔ l2) → UU l3) {A : UU l1} {B : UU l2} (f : A → B) → UU (l2 ⊔ l3) -structure-map P {A} {B} f = (b : B) → P (fiber f b) +structure-map 𝒫 {A} {B} f = (b : B) → 𝒫 (fiber f b) hom-structure : - {l1 l2 l3 : Level} (P : UU (l1 ⊔ l2) → UU l3) → + {l1 l2 l3 : Level} (𝒫 : UU (l1 ⊔ l2) → UU l3) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ l3) -hom-structure P A B = Σ (A → B) (structure-map P) +hom-structure 𝒫 A B = Σ (A → B) (structure-map 𝒫) + +structure-equality : + {l1 l2 : Level} (𝒫 : UU l1 → UU l2) → UU l1 → UU (l1 ⊔ l2) +structure-equality 𝒫 A = (x y : A) → 𝒫 (x ＝ y) ``` ## Properties ### Having structure is closed under equivalences +This is a consequence of [the univalence axiom](foundation.univalence.md) + ```agda has-structure-equiv : - {l1 l2 : Level} (P : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → P X → P Y -has-structure-equiv P e = tr P (eq-equiv e) + {l1 l2 : Level} (𝒫 : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → 𝒫 X → 𝒫 Y +has-structure-equiv 𝒫 e = tr 𝒫 (eq-equiv e) has-structure-equiv' : - {l1 l2 : Level} (P : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → P Y → P X -has-structure-equiv' P e = tr P (inv (eq-equiv e)) + {l1 l2 : Level} (𝒫 : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → 𝒫 Y → 𝒫 X +has-structure-equiv' 𝒫 e = tr 𝒫 (inv (eq-equiv e)) ``` From f37ef8853edddb7a0126bc7cfdcb7a39b9966ed0 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 18:39:54 +0100 Subject: [PATCH 11/23] the strong preunivalence axiom --- src/foundation.lagda.md | 1 + ...orem-of-identity-types-structures.lagda.md | 2 +- src/foundation/preunivalence.lagda.md | 1 + src/foundation/strong-preunivalence.lagda.md | 144 ++++++++++++++++++ 4 files changed, 147 insertions(+), 1 deletion(-) create mode 100644 src/foundation/strong-preunivalence.lagda.md diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index c4b3747dbe..633cd34058 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -393,6 +393,7 @@ 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 diff --git a/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md b/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md index a80dea8713..b1ae74c613 100644 --- a/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md +++ b/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md @@ -12,8 +12,8 @@ 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.structure +open import foundation.subuniverses open import foundation.universe-levels open import foundation-core.contractible-types diff --git a/src/foundation/preunivalence.lagda.md b/src/foundation/preunivalence.lagda.md index 298f482891..9fe3c4409c 100644 --- a/src/foundation/preunivalence.lagda.md +++ b/src/foundation/preunivalence.lagda.md @@ -107,5 +107,6 @@ preunivalence = preunivalence-axiom-univalence-axiom univalence - Preunivalence is sufficient to prove that `Id : A → (A → 𝒰)` is an embedding. This fact is proven in [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md) +- [The strong preunivalence axiom](foundation.strong-preunivalence.md) - [Preunivalent type families](foundation.preunivalent-type-families.md) - [Preunivalent categories](category-theory.preunivalent-categories.md) diff --git a/src/foundation/strong-preunivalence.lagda.md b/src/foundation/strong-preunivalence.lagda.md new file mode 100644 index 0000000000..b71fa5963b --- /dev/null +++ b/src/foundation/strong-preunivalence.lagda.md @@ -0,0 +1,144 @@ +# The strong preunivalence axiom + +```agda +module foundation.strong-preunivalence where +``` + +
Imports + +```agda +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.functoriality-dependent-pair-types +open import foundation.fundamental-theorem-of-identity-types-structures +open import foundation.preunivalence +open import foundation.propositional-maps +open import foundation.propositions +open import foundation.sets +open import foundation.small-types +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.function-types +open import foundation-core.identity-types +open import foundation-core.subtypes +``` + +
+ +## Idea + +{{#concept "The strong preunivalence axiom" Agda=strong-preunivalence-axiom}} is +a common generalization of the [univalence axiom](foundation.univalence.md) and +[axiom K](foundation-core.sets.md). It asserts that for any type `X : 𝒰` and any +other universe `𝒱`, the [smallness predicate](foundation-core.small-types.md) +`is-small 𝒱 X ≐ Σ (Y : 𝒱), (X ≃ Y)` is a [set](foundation-core.sets.md). + +The strong preunivalence axiom is a strengthening of +[the preunivalence axiom](foundation.preunivalence.md) in the following way. If +we restrict to `𝒱 ≐ 𝒰`, the +[fundamental theorem of identity types for subuniverses](foundation.fundamental-theorem-of-identity-types-subuniverses.md) +says that `Σ (Y : 𝒰), (X ≃ Y)` is a set if and only if _every_ binary family of +maps + +```text + (X Y : 𝒰) → (X ＝ Y) → (X ≃ Y) +``` + +is a family of [embeddings](foundation-core.embeddings.md). The preunivalence +axiom asserts that the particular binary family of maps defined by identity +induction as `refl ↦ id-equiv` is an embedding. + +While the strong preunivalence axiom is a strengthening of the preunivalence +axiom, it is still common generalization of the +[univalence axiom](foundation.univalence.md) and +[axiom K](foundation-core.sets.md). If we assume the univalence axiom then +`is-small` is a proposition, and if we assume axiom K then every type is a set. + +## Definitions + +```agda +instance-strong-preunivalence : + {l1 : Level} (l2 : Level) (X : UU l1) → UU (l1 ⊔ lsuc l2) +instance-strong-preunivalence l2 X = is-set (is-small l2 X) + +strong-preunivalence-axiom-Level : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +strong-preunivalence-axiom-Level l1 l2 = + (X : UU l1) → instance-strong-preunivalence l2 X + +strong-preunivalence-axiom : UUω +strong-preunivalence-axiom = + {l1 l2 : Level} → strong-preunivalence-axiom-Level l1 l2 +``` + +## Properties + +### The strong preunivalence axiom strengthens the preunivalence axiom + +```agda +based-preunivalence-instance-strong-preunivalence : + {l : Level} (X : UU l) → + instance-strong-preunivalence l X → based-preunivalence-axiom X +based-preunivalence-instance-strong-preunivalence X L Y = + is-emb-is-prop-map + ( backward-implication-fundamental-theorem-unbased-id-subuniverse + ( is-prop-Prop) + ( L) + ( X) + ( λ _ → equiv-eq) + ( Y)) + +preunivalence-axiom-strong-preunivalence-axiom : + strong-preunivalence-axiom → preunivalence-axiom +preunivalence-axiom-strong-preunivalence-axiom L X = + based-preunivalence-instance-strong-preunivalence X (L X) +``` + +### The strong preunivalence axiom generalizes axiom K + +To show that preunivalence generalizes axiom K, we assume axiom K for the types +in question and for the universe itself. + +```agda +instance-strong-preunivalence-instance-axiom-K : + {l1 : Level} (l2 : Level) (A : UU l1) → + instance-axiom-K (UU l2) → + ((B : UU l2) → instance-axiom-K (A ≃ B)) → + instance-strong-preunivalence l2 A +instance-strong-preunivalence-instance-axiom-K l2 A K-Type K-A≃B = + is-set-Σ (is-set-axiom-K K-Type) (is-set-axiom-K ∘ K-A≃B) + +strong-preunivalence-axiom-axiom-K : axiom-K → strong-preunivalence-axiom +strong-preunivalence-axiom-axiom-K K {l1} {l2} A = + instance-strong-preunivalence-instance-axiom-K l2 A + ( K (UU l2)) + ( λ B → K (A ≃ B)) +``` + +### The strong preunivalence axiom generalizes the univalence axiom + +```agda +strong-preunivalence-axiom-univalence-axiom : + univalence-axiom → strong-preunivalence-axiom +strong-preunivalence-axiom-univalence-axiom UA {l1} {l2} A = + is-set-is-prop + ( is-prop-is-proof-irrelevant + ( λ (X , e) → + is-contr-equiv' + ( is-small l2 X) + ( equiv-tot (equiv-precomp-equiv e)) + ( is-torsorial-equiv-based-univalence X (UA X)))) +``` + +### Strong preunivalence holds in univalent foundations + +```agda +strong-preunivalence : strong-preunivalence-axiom +strong-preunivalence = strong-preunivalence-axiom-univalence-axiom univalence +``` + +## See also + +- [Preunivalent categories](category-theory.preunivalent-categories.md) From 231f43b2e3173f646de7b31f4cbb74ed82a3c613 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 18:47:04 +0100 Subject: [PATCH 12/23] a choice of word --- src/foundation-core/equality-dependent-pair-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md index 5668a7cc6e..bcc2650afd 100644 --- a/src/foundation-core/equality-dependent-pair-types.lagda.md +++ b/src/foundation-core/equality-dependent-pair-types.lagda.md @@ -168,7 +168,7 @@ module _ ap-pr1-eq-pair-Σ refl refl = refl ``` -### Transporting in `B` along the first projection of an identification in `Σ A B` +### Transport in `B` along the first projection of an identification in `Σ A B` ```agda module _ From b50fde7db1b67fe13dd548fb4aed0b5585635fd8 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 19:11:20 +0100 Subject: [PATCH 13/23] rename to "structured equality duality" --- src/foundation.lagda.md | 2 +- src/foundation/strong-preunivalence.lagda.md | 4 +- ...d => structured-equality-duality.lagda.md} | 64 +++++++++---------- 3 files changed, 35 insertions(+), 35 deletions(-) rename src/foundation/{fundamental-theorem-of-identity-types-structures.lagda.md => structured-equality-duality.lagda.md} (58%) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 633cd34058..1f6f173430 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -211,7 +211,6 @@ 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 @@ -397,6 +396,7 @@ 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 diff --git a/src/foundation/strong-preunivalence.lagda.md b/src/foundation/strong-preunivalence.lagda.md index b71fa5963b..467474a775 100644 --- a/src/foundation/strong-preunivalence.lagda.md +++ b/src/foundation/strong-preunivalence.lagda.md @@ -12,12 +12,12 @@ open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.functoriality-dependent-pair-types -open import foundation.fundamental-theorem-of-identity-types-structures open import foundation.preunivalence open import foundation.propositional-maps open import foundation.propositions open import foundation.sets open import foundation.small-types +open import foundation.structured-equality-duality open import foundation.univalence open import foundation.universe-levels @@ -83,7 +83,7 @@ based-preunivalence-instance-strong-preunivalence : instance-strong-preunivalence l X → based-preunivalence-axiom X based-preunivalence-instance-strong-preunivalence X L Y = is-emb-is-prop-map - ( backward-implication-fundamental-theorem-unbased-id-subuniverse + ( backward-implication-subuniverse-equality-duality ( is-prop-Prop) ( L) ( X) diff --git a/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md b/src/foundation/structured-equality-duality.lagda.md similarity index 58% rename from src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md rename to src/foundation/structured-equality-duality.lagda.md index b1ae74c613..b82ade56cd 100644 --- a/src/foundation/fundamental-theorem-of-identity-types-structures.lagda.md +++ b/src/foundation/structured-equality-duality.lagda.md @@ -1,7 +1,7 @@ -# The fundamental theorem of identity types for structures +# Structured equality duality ```agda -module foundation.fundamental-theorem-of-identity-types-structures where +module foundation.structured-equality-duality where ```
Imports @@ -33,18 +33,16 @@ open import foundation-core.torsorial-type-families ## Idea -> TODO +Given a [structure](foundation.structure.md) `𝒫` on types that transfers along +[equivalences](foundation-core.equivalences.md), then for every type `A` and +type family `B : A → 𝒰` there is a +[mutual correspondence](foundation.logical-equivalences.md) between -## Theorem +1. For every `x : A`, `𝒫`-structured families of maps + `f : (y : A) → (x ＝ y) → B y`. +2. `𝒫`-structures on the equality of `Σ A B`. -### The unbased fundamental theorem of identity types for structures - -Given a structure `𝒫` on types that transports along equivalences, then the -following are logically equivalent: - -1. For every `x : A`, every family of maps map out of the identity types of `A`, - `f : (y : A) → (x ＝ y) → B y` is `𝒫`-structured. -2. The identity types of `Σ A B` are `𝒫`-structured. +## Construction ```agda module _ @@ -53,37 +51,39 @@ module _ {A : UU l1} {B : A → UU l2} where - forward-implication-fundamental-theorem-unbased-id-structure : + forward-implication-structured-equality-duality : ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) → structure-equality 𝒫 (Σ A B) - forward-implication-fundamental-theorem-unbased-id-structure + forward-implication-structured-equality-duality 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 : + backward-implication-structured-equality-duality : structure-equality 𝒫 (Σ A B) → ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) - backward-implication-fundamental-theorem-unbased-id-structure K x f y b = + backward-implication-structured-equality-duality 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 : + structured-equality-duality : ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) ↔ ( structure-equality 𝒫 (Σ A B)) - fundamental-theorem-unbased-id-structure = - ( forward-implication-fundamental-theorem-unbased-id-structure , - backward-implication-fundamental-theorem-unbased-id-structure) + structured-equality-duality = + ( forward-implication-structured-equality-duality , + backward-implication-structured-equality-duality) ``` -### The unbased fundamental theorem of identity types for subuniverses +## Corollaries + +### Subuniverse equality duality 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 `𝒫`. +1. For every `x : A`, every family of maps `f : (y : A) → (x ＝ y) → B y` is a + family of `𝒫`-maps. 2. The dependent sum `Σ A B` is `𝒫`-separated. ```agda @@ -93,28 +93,28 @@ module _ where abstract - forward-implication-fundamental-theorem-unbased-id-subuniverse : + forward-implication-subuniverse-equality-duality : ( (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 + forward-implication-subuniverse-equality-duality = + forward-implication-structured-equality-duality ( is-in-subuniverse-equiv 𝒫) abstract - backward-implication-fundamental-theorem-unbased-id-subuniverse : + backward-implication-subuniverse-equality-duality : 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 + backward-implication-subuniverse-equality-duality = + backward-implication-structured-equality-duality ( is-in-subuniverse-equiv 𝒫) abstract - fundamental-theorem-unbased-id-subuniverse : + subuniverse-equality-duality : ( (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 𝒫) + subuniverse-equality-duality = + structured-equality-duality (is-in-subuniverse-equiv 𝒫) ``` From 0744c3f2937a297c47b88ea412157d5f6b97f3f7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 19:28:12 +0100 Subject: [PATCH 14/23] citations and a historical correction --- references.bib | 10 +++++++ ...universal-property-identity-types.lagda.md | 26 ++++++++++--------- 2 files changed, 24 insertions(+), 12 deletions(-) diff --git a/references.bib b/references.bib index 2c7232900e..938394ca2d 100644 --- a/references.bib +++ b/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}, diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md index eafff48723..f8563b3fad 100644 --- a/src/foundation/universal-property-identity-types.lagda.md +++ b/src/foundation/universal-property-identity-types.lagda.md @@ -120,11 +120,11 @@ We first show that [injectivity](foundation-core.injective-maps.md) of the map ``` for the identity types of `A` implies that the map `Id : A → (A → 𝒰)` is an -[embedding](foundation.embeddings.md). Since the -[univalence axiom](foundation.univalence.md) implies -[the preunivalence axiom](foundation.preunivalence.md) implies injectivity of -`equiv-eq`, it follows that `Id : A → (A → 𝒰)` is an embedding under the -postulates of agda-unimath. +[embedding](foundation.embeddings.md), a result due to Martín Escardó +{{#cite TypeTopology}}. Since the [univalence axiom](foundation.univalence.md) +implies [the preunivalence axiom](foundation.preunivalence.md) implies +injectivity of `equiv-eq`, it follows that `Id : A → (A → 𝒰)` is an embedding +under the postulates of agda-unimath. #### Injectivity of `equiv-eq` implies `Id : A → (A → 𝒰)` is an embedding @@ -322,14 +322,16 @@ module _ - In [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md) - we will show that the fiber of `Id : A → (A → 𝒰)` at `B : A → 𝒰` is equivalent - to `is-torsorial B`. + we show that the fiber of `Id : A → (A → 𝒰)` at `B : A → 𝒰` is equivalent to + `is-torsorial B`. ## References -- The fact that preunivalence, or axiom L, is sufficient to prove that - `Id : A → (A → 𝒰)` is an embedding was first observed and formalized by Martín - Escardó, - [https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html](https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html). +It was first observed and proved by Evan Cavallo that preunivalence, or Axiom L, +is sufficient to deduce that `Id : A → (A → 𝒰)` is an embedding. It was later +observed and formalized by Martín Escardó that assuming the map +`equiv-eq : (X ＝ Y) → (X ≃ Y)` is injective is enough. {{#cite TypeTopology}} +Martín Escardó formalizations can be found here: +[https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html](https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html). -{{#bibliography}} {{#reference TypeTopology}} +{{#bibliography}} {{#reference TypeTopology}} {{#reference Esc17YetAnother}} From c2f255e6fd7fa4360157e7e14296be6109fc9cf2 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 20:04:24 +0100 Subject: [PATCH 15/23] strengthen definition of preunivalent category --- src/category-theory/categories.lagda.md | 10 +- .../indiscrete-precategories.lagda.md | 6 +- .../opposite-preunivalent-categories.lagda.md | 19 ++- .../preunivalent-categories.lagda.md | 112 +++++++++++++----- .../strict-categories.lagda.md | 10 +- 5 files changed, 107 insertions(+), 50 deletions(-) diff --git a/src/category-theory/categories.lagda.md b/src/category-theory/categories.lagda.md index 810689aba3..81114b2cc7 100644 --- a/src/category-theory/categories.lagda.md +++ b/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) → diff --git a/src/category-theory/indiscrete-precategories.lagda.md b/src/category-theory/indiscrete-precategories.lagda.md index 68479adbd5..02f42fb044 100644 --- a/src/category-theory/indiscrete-precategories.lagda.md +++ b/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})) diff --git a/src/category-theory/opposite-preunivalent-categories.lagda.md b/src/category-theory/opposite-preunivalent-categories.lagda.md index 4ea17ae265..2819a2d057 100644 --- a/src/category-theory/opposite-preunivalent-categories.lagda.md +++ b/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 : diff --git a/src/category-theory/preunivalent-categories.lagda.md b/src/category-theory/preunivalent-categories.lagda.md index 9f593f0cbe..e5cff574ea 100644 --- a/src/category-theory/preunivalent-categories.lagda.md +++ b/src/category-theory/preunivalent-categories.lagda.md @@ -15,10 +15,13 @@ 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 ``` @@ -26,34 +29,41 @@ open import foundation.universe-levels ## 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 +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). + +The preunivalence condition on precategories states that every way to display +the type of objects over the groupoid of isomorphisms is a subgroupoid. For +univalent categories every way to display its objects over the groupoid of +isomorphisms is trivial, 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. +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. ## Definitions ### The predicate on precategories of being a preunivalent category +We define preunivalence of a category `𝒞` to be the condition that every type of +the form `Σ (x : 𝒞₀), (x ≅ y)` is a set. + ```agda module _ {l1 l2 : Level} (C : Precategory l1 l2) @@ -64,12 +74,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 +191,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 +309,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 diff --git a/src/category-theory/strict-categories.lagda.md b/src/category-theory/strict-categories.lagda.md index d26990c1f5..66a81cdc1c 100644 --- a/src/category-theory/strict-categories.lagda.md +++ b/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 From 71a526abcf77140acea4e8e51e2ed1c1434c8b6f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 20:40:38 +0100 Subject: [PATCH 16/23] self-review --- .../preunivalent-type-families.lagda.md | 7 +- ...amental-theorem-of-identity-types.lagda.md | 8 +-- src/foundation/strong-preunivalence.lagda.md | 18 ++--- ...universal-property-identity-types.lagda.md | 69 +++++++++---------- 4 files changed, 50 insertions(+), 52 deletions(-) diff --git a/src/foundation/preunivalent-type-families.lagda.md b/src/foundation/preunivalent-type-families.lagda.md index 96fb37312b..933a182ad5 100644 --- a/src/foundation/preunivalent-type-families.lagda.md +++ b/src/foundation/preunivalent-type-families.lagda.md @@ -39,7 +39,12 @@ the map equiv-tr B : x ＝ y → B x ≃ B y ``` -is an [embedding](foundation-core.embeddings.md) for every `x y : A`. +is an [embedding](foundation-core.embeddings.md) for every `x y : A`. By +[the preunivalence axiom](foundation.preunivalence.md), which follows from +[the univalence axiom](foundation.univalence.md), the type family `B` is +preunivalent if and only if it is [faithful](foundation.faithful-maps.md) as a +map. In other words, if `A` is a [set](foundation-core.sets.md)-level +[structure](foundation.structure.md) on types. ## Definition diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index 3450987fe8..cfc3c9d40b 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -131,10 +131,10 @@ module _ ### The unbased extended fundamental theorem of identity types -We can give a similar characterization for a binary family of types -`B : A → A → 𝒰` over a not necessarily pointed or inhabited type `A` whose -elements are all merely equal. In other words, `A` is any π₀-trivial type. The -characterization asserts that the following are equivalent: +We give a similar characterization for a binary family of types `B : A → A → 𝒰` +over a not necessarily pointed or inhabited type `A` whose elements are all +merely equal. In other words, `A` is any π₀-trivial type. The characterization +asserts that the following are equivalent: 1. For every `x : A` and every family of maps out of the identity types `f : (y : A) → (x ＝ y) → B x y`, then for every `y : A` the `f y` is a diff --git a/src/foundation/strong-preunivalence.lagda.md b/src/foundation/strong-preunivalence.lagda.md index 467474a775..4a941614f7 100644 --- a/src/foundation/strong-preunivalence.lagda.md +++ b/src/foundation/strong-preunivalence.lagda.md @@ -38,23 +38,23 @@ other universe `𝒱`, the [smallness predicate](foundation-core.small-types.md) The strong preunivalence axiom is a strengthening of [the preunivalence axiom](foundation.preunivalence.md) in the following way. If -we restrict to `𝒱 ≐ 𝒰`, the -[fundamental theorem of identity types for subuniverses](foundation.fundamental-theorem-of-identity-types-subuniverses.md) -says that `Σ (Y : 𝒰), (X ≃ Y)` is a set if and only if _every_ binary family of -maps +we restrict to `𝒱 ≐ 𝒰`, +[subuniverse equality duality](foundation.structured-equality-duality.md) says +that `Σ (Y : 𝒰), (X ≃ Y)` is a set if and only if every binary family of maps ```text - (X Y : 𝒰) → (X ＝ Y) → (X ≃ Y) + (Z Y : 𝒰) → (Z ＝ Y) → (X ≃ Y) ``` -is a family of [embeddings](foundation-core.embeddings.md). The preunivalence -axiom asserts that the particular binary family of maps defined by identity -induction as `refl ↦ id-equiv` is an embedding. +is a binary family of [embeddings](foundation-core.embeddings.md). The +preunivalence axiom asserts that the particular family of maps +`(Y : 𝒰) → (X ＝ Y) → (X ≃ Y)` defined by identity induction as +`refl ↦ id-equiv` is a family of embeddings. While the strong preunivalence axiom is a strengthening of the preunivalence axiom, it is still common generalization of the [univalence axiom](foundation.univalence.md) and -[axiom K](foundation-core.sets.md). If we assume the univalence axiom then +[axiom K](foundation-core.sets.md): if we assume the univalence axiom then `is-small` is a proposition, and if we assume axiom K then every type is a set. ## Definitions diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md index f8563b3fad..33eb341448 100644 --- a/src/foundation/universal-property-identity-types.lagda.md +++ b/src/foundation/universal-property-identity-types.lagda.md @@ -145,14 +145,15 @@ Since the codomain of this injection is contractible, the claim follows. The above injection is constructed as the following composite injection ```text - Σ (x : A), Id x ＝ Id a + Σ (x : A), Id a ＝ Id x + ≃ Σ (x : A), Id x ＝ Id a ≃ Σ (x : A), ((y : A) → (x ＝ y) ＝ (a ＝ y)) ↣ Σ (x : A), ((y : A) → (x ＝ y) ≃ (a ＝ y)) - ↪ Σ (x : A), ((y : A) → (x ＝ y) → (a ＝ y)) + ≃ Σ (x : A), ((y : A) → (x ＝ y) → (a ＝ y)) ≃ Σ (x : A), a ＝ x. ``` -In this composite, the injectivity of `equiv-eq` is used in the second step. +In this composite, the injectivity of `equiv-eq` is used in the third step. ```agda module _ @@ -160,22 +161,21 @@ module _ (L : (a x y : A) → is-injective (equiv-eq {A = Id x y} {B = Id a y})) where + injection-Id-is-injective-equiv-eq-Id : + (a x : A) → injection (Id a ＝ Id x) (a ＝ x) + injection-Id-is-injective-equiv-eq-Id a x = + comp-injection + ( injection-equiv + ( ( equiv-ev-refl x) ∘e + ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a)))) + ( comp-injection + ( injection-Π (λ y → _ , L a x y)) + ( injection-equiv (equiv-funext ∘e equiv-inv (Id a) (Id x)))) + injection-fiber-Id-is-injective-equiv-eq-Id : (a : A) → injection (fiber' Id (Id a)) (Σ A (Id a)) injection-fiber-Id-is-injective-equiv-eq-Id a = - comp-injection - ( comp-injection - ( injection-equiv - ( equiv-tot - ( λ x → - ( equiv-ev-refl x) ∘e - ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a))))) - ( injection-tot - ( λ x → - comp-injection - ( injection-Π (λ y → _ , L a x y)) - ( injection-equiv equiv-funext)))) - ( injection-equiv (inv-equiv (equiv-fiber Id (Id a)))) + injection-tot (injection-Id-is-injective-equiv-eq-Id a) is-emb-Id-is-injective-equiv-eq-Id : is-emb (Id {A = A}) is-emb-Id-is-injective-equiv-eq-Id a = @@ -206,21 +206,19 @@ module _ (L : (a x y : A) → instance-preunivalence (Id x y) (Id a y)) where - emb-fiber-Id-preunivalent-Id : (a : A) → fiber' Id (Id a) ↪ Σ A (Id a) - emb-fiber-Id-preunivalent-Id a = + emb-Id-is-injective-equiv-eq-Id : (a x : A) → (Id a ＝ Id x) ↪ (a ＝ x) + emb-Id-is-injective-equiv-eq-Id a x = comp-emb + ( emb-equiv + ( ( equiv-ev-refl x) ∘e + ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a)))) ( comp-emb - ( emb-equiv - ( equiv-tot - ( λ x → - ( equiv-ev-refl x) ∘e - ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a))))) - ( emb-tot - ( λ x → - comp-emb - ( emb-Π (λ y → _ , L a x y)) - ( emb-equiv equiv-funext)))) - ( emb-equiv (inv-equiv (equiv-fiber Id (Id a)))) + ( emb-Π (λ y → _ , L a x y)) + ( emb-equiv (equiv-funext ∘e equiv-inv (Id a) (Id x)))) + + emb-fiber-Id-preunivalent-Id : (a : A) → fiber' Id (Id a) ↪ Σ A (Id a) + emb-fiber-Id-preunivalent-Id a = + emb-tot (emb-Id-is-injective-equiv-eq-Id a) is-emb-Id-preunivalent-Id : is-emb (Id {A = A}) is-emb-Id-preunivalent-Id = @@ -295,15 +293,12 @@ module _ abstract is-torsorial-pointed-fam-equiv-is-torsorial : - is-torsorial - ( λ (e : (x : A) → (a ＝ x) ≃ B x) → - map-equiv (e a) refl ＝ b) + is-torsorial (λ (e : (x : A) → (a ＝ x) ≃ B x) → map-equiv (e a) refl ＝ b) is-torsorial-pointed-fam-equiv-is-torsorial = is-contr-equiv' - ( fiber (ev-refl a {B = λ x _ → B x}) b) + ( fiber (ev-refl a) b) ( equiv-Σ _ - ( inv-equiv - ( equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B)) + ( inv-equiv (equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B)) ( λ h → equiv-inv-concat ( inv @@ -313,9 +308,7 @@ module _ ( equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B) ( h)))) ( b))) - ( is-contr-map-is-equiv - ( is-equiv-ev-refl a) - ( b)) + ( is-contr-map-is-equiv (is-equiv-ev-refl a) b) ``` ## See also From d88be880ed31273049229d2b96ca1af8ac39da61 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 20:48:59 +0100 Subject: [PATCH 17/23] remove redundant text --- src/category-theory/preunivalent-categories.lagda.md | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/category-theory/preunivalent-categories.lagda.md b/src/category-theory/preunivalent-categories.lagda.md index e5cff574ea..735c872f1f 100644 --- a/src/category-theory/preunivalent-categories.lagda.md +++ b/src/category-theory/preunivalent-categories.lagda.md @@ -48,15 +48,6 @@ however, that our definition of preunivalence here is a [strengthening](foundation.strong-preunivalence.md) of the [preunivalence axiom](foundation.preunivalence.md). -The preunivalence condition on precategories states that every way to display -the type of objects over the groupoid of isomorphisms is a subgroupoid. For -univalent categories every way to display its objects over the groupoid of -isomorphisms is trivial, 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. - ## Definitions ### The predicate on precategories of being a preunivalent category From 0f950e2f73018228001da0f678cd346d47876bf5 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Jan 2025 20:50:33 +0100 Subject: [PATCH 18/23] fix a sentence --- src/category-theory/preunivalent-categories.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/category-theory/preunivalent-categories.lagda.md b/src/category-theory/preunivalent-categories.lagda.md index 735c872f1f..0b283e3c0b 100644 --- a/src/category-theory/preunivalent-categories.lagda.md +++ b/src/category-theory/preunivalent-categories.lagda.md @@ -52,8 +52,8 @@ however, that our definition of preunivalence here is a ### The predicate on precategories of being a preunivalent category -We define preunivalence of a category `𝒞` to be the condition that every type of -the form `Σ (x : 𝒞₀), (x ≅ y)` is a set. +We define preunivalence of a precategory `𝒞` to be the condition that for every +`x : 𝒞₀`, the type `Σ (y : 𝒞₀), (x ≅ y)` is a set. ```agda module _ From 13d1eaf53b3c7356d500f3a188b4bbf506f229ea Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Jan 2025 00:41:20 +0100 Subject: [PATCH 19/23] review --- ...amental-theorem-of-identity-types.lagda.md | 77 +++++++++---------- src/foundation/strong-preunivalence.lagda.md | 3 - .../structured-equality-duality.lagda.md | 29 +++---- ...universal-property-identity-types.lagda.md | 33 +++++--- .../lifts-families-of-elements.lagda.md | 4 +- ...sition-lifts-families-of-elements.lagda.md | 2 +- .../flattening-lemma-coequalizers.lagda.md | 2 +- 7 files changed, 78 insertions(+), 72 deletions(-) diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index cfc3c9d40b..5381fa28bb 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -28,6 +28,7 @@ open import foundation.maps-in-subuniverses open import foundation.mere-equality open import foundation.propositional-truncations open import foundation.separated-types-subuniverses +open import foundation.structured-equality-duality open import foundation.subuniverses open import foundation.surjective-maps open import foundation.truncated-maps @@ -40,7 +41,8 @@ open import foundation.universe-levels ## Idea -The **Regensburg extension** of the +The {{#concept "Regensburg extension" Agda=extended-fundamental-theorem-id}} of +the [fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md) asserts that for any [subuniverse](foundation.subuniverses.md) `P`, and any [pointed](structured-types.pointed-types.md) @@ -87,46 +89,37 @@ agda-unimath. ```agda module _ - {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) + {l1 l2 l3 : Level} (𝒫 : subuniverse (l1 ⊔ l2) l3) {A : UU l1} (a : A) {B : A → UU l2} where abstract forward-implication-extended-fundamental-theorem-id : is-0-connected A → - ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map P (f x)) → - is-separated P (Σ A B) - 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 ((x , y) ＝ (x' , y'))) - ( λ where - refl → - is-in-subuniverse-equiv P - ( compute-fiber-map-out-of-identity-type - ( ind-Id a (λ u _ → B u) y) - ( x') - ( y')) - ( K (ind-Id a (λ u _ → B u) y) x' y')) + ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map 𝒫 (f x)) → + is-separated 𝒫 (Σ A B) + forward-implication-extended-fundamental-theorem-id H K = + forward-implication-subuniverse-equality-duality 𝒫 + ( λ x f y b → + apply-universal-property-trunc-Prop + ( mere-eq-is-0-connected H a x) + ( 𝒫 (fiber (f y) b)) + ( λ where refl → K f y b)) abstract backward-implication-extended-fundamental-theorem-id : - is-separated P (Σ A B) → - (f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map P (f x) - backward-implication-extended-fundamental-theorem-id K f x y = - is-in-subuniverse-equiv' P - ( compute-fiber-map-out-of-identity-type f x y) - ( K (a , f a refl) (x , y)) + is-separated 𝒫 (Σ A B) → + (f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map 𝒫 (f x) + backward-implication-extended-fundamental-theorem-id K = + backward-implication-subuniverse-equality-duality 𝒫 K a - abstract - extended-fundamental-theorem-id : - is-0-connected A → - ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map P (f x)) ↔ - is-separated P (Σ A B) - pr1 (extended-fundamental-theorem-id H) = - forward-implication-extended-fundamental-theorem-id H - pr2 (extended-fundamental-theorem-id H) = - backward-implication-extended-fundamental-theorem-id + extended-fundamental-theorem-id : + is-0-connected A → + ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map 𝒫 (f x)) ↔ + is-separated 𝒫 (Σ A B) + extended-fundamental-theorem-id H = + ( forward-implication-extended-fundamental-theorem-id H , + backward-implication-extended-fundamental-theorem-id) ``` ### The unbased extended fundamental theorem of identity types @@ -138,38 +131,38 @@ asserts that the following are equivalent: 1. For every `x : A` and every family of maps out of the identity types `f : (y : A) → (x ＝ y) → B x y`, then for every `y : A` the `f y` is a - `P`-map. -2. For every `x : A` the type `Σ A (B x)` is `P`-separated. + `𝒫`-map. +2. For every `x : A` the type `Σ A (B x)` is `𝒫`-separated. ```agda module _ - {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) + {l1 l2 l3 : Level} (𝒫 : subuniverse (l1 ⊔ l2) l3) {A : UU l1} {B : A → A → UU l2} where forward-implication-extended-fundamental-theorem-unbased-id : ( (x y : A) → mere-eq x y) → ( (x : A) (f : (y : A) → (x ＝ y) → B x y) - (y : A) → is-in-subuniverse-map P (f y)) → - ( (x : A) → is-separated P (Σ A (B x))) + (y : A) → is-in-subuniverse-map 𝒫 (f y)) → + ( (x : A) → is-separated 𝒫 (Σ A (B x))) forward-implication-extended-fundamental-theorem-unbased-id H K x = - forward-implication-extended-fundamental-theorem-id P + forward-implication-extended-fundamental-theorem-id 𝒫 ( x) ( is-0-connected-mere-eq x (H x)) ( K x) backward-implication-extended-fundamental-theorem-unbased-id : - ( (x : A) → is-separated P (Σ A (B x))) → + ( (x : A) → is-separated 𝒫 (Σ A (B x))) → ( (x : A) (f : (y : A) → (x ＝ y) → B x y) - (y : A) → is-in-subuniverse-map P (f y)) + (y : A) → is-in-subuniverse-map 𝒫 (f y)) backward-implication-extended-fundamental-theorem-unbased-id K x = - backward-implication-extended-fundamental-theorem-id P x (K x) + backward-implication-extended-fundamental-theorem-id 𝒫 x (K x) extended-fundamental-theorem-unbased-id : ( (x y : A) → mere-eq x y) → ( (x : A) (f : (y : A) → (x ＝ y) → B x y) - (y : A) → is-in-subuniverse-map P (f y)) ↔ - ( (x : A) → is-separated P (Σ A (B x))) + (y : A) → is-in-subuniverse-map 𝒫 (f y)) ↔ + ( (x : A) → is-separated 𝒫 (Σ A (B x))) extended-fundamental-theorem-unbased-id H = ( forward-implication-extended-fundamental-theorem-unbased-id H , backward-implication-extended-fundamental-theorem-unbased-id) diff --git a/src/foundation/strong-preunivalence.lagda.md b/src/foundation/strong-preunivalence.lagda.md index 4a941614f7..d0a32feb13 100644 --- a/src/foundation/strong-preunivalence.lagda.md +++ b/src/foundation/strong-preunivalence.lagda.md @@ -9,7 +9,6 @@ module foundation.strong-preunivalence where ```agda open import foundation.contractible-types open import foundation.dependent-pair-types -open import foundation.embeddings open import foundation.equivalences open import foundation.functoriality-dependent-pair-types open import foundation.preunivalence @@ -22,8 +21,6 @@ open import foundation.univalence open import foundation.universe-levels open import foundation-core.function-types -open import foundation-core.identity-types -open import foundation-core.subtypes ```
diff --git a/src/foundation/structured-equality-duality.lagda.md b/src/foundation/structured-equality-duality.lagda.md index b82ade56cd..88ef8a17bd 100644 --- a/src/foundation/structured-equality-duality.lagda.md +++ b/src/foundation/structured-equality-duality.lagda.md @@ -16,17 +16,7 @@ open import foundation.structure 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 ```
@@ -36,12 +26,17 @@ open import foundation-core.torsorial-type-families Given a [structure](foundation.structure.md) `𝒫` on types that transfers along [equivalences](foundation-core.equivalences.md), then for every type `A` and type family `B : A → 𝒰` there is a -[mutual correspondence](foundation.logical-equivalences.md) between +[mutual correspondence](foundation.logical-equivalences.md) between the +following: -1. For every `x : A`, `𝒫`-structured families of maps - `f : (y : A) → (x ＝ y) → B y`. +1. `𝒫`-structured binary families of maps `f : (y : A) → (x ＝ y) → B y`. 2. `𝒫`-structures on the equality of `Σ A B`. +Note that, by [univalence axiom](foundation.univalence.md), every structure +[transfers along equivalences](foundation.transport-along-equivalences.md). +However, we maintain this as an assumption, since for most common notions of +structure this property is independent of the univalence axiom. + ## Construction ```agda @@ -118,3 +113,11 @@ module _ subuniverse-equality-duality = structured-equality-duality (is-in-subuniverse-equiv 𝒫) ``` + +## See also + +This duality is applied in + +- [The Regensburg extension of the fundamental theorem of identity types](foundation.regensburg-extension-fundamental-theorem-of-identity-types.md) +- [The strong preunivalence axiom](foundation.strong-preunivalence.md) +- [Preunivalent categories](category-theory.preunivalent-categories.md) diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md index 33eb341448..a970aa460e 100644 --- a/src/foundation/universal-property-identity-types.lagda.md +++ b/src/foundation/universal-property-identity-types.lagda.md @@ -38,9 +38,10 @@ open import foundation-core.torsorial-type-families ## Idea -The {{#concept "universal property of identity types"}} characterizes families -of maps out of the [identity type](foundation-core.identity-types.md). This -universal property is also known as the **type theoretic Yoneda lemma**. +The {{#concept "universal property of identity types" Agda=equiv-eq-refl}} +characterizes families of maps out of the +[identity type](foundation-core.identity-types.md). This universal property is +also known as the **type theoretic Yoneda lemma**. ## Theorem @@ -116,7 +117,7 @@ module _ We first show that [injectivity](foundation-core.injective-maps.md) of the map ```text - equiv-eq : {X Y : 𝓤} → (X ＝ Y) → (X ≃ Y) + equiv-eq : {X Y : 𝒰} → (X ＝ Y) → (X ≃ Y) ``` for the identity types of `A` implies that the map `Id : A → (A → 𝒰)` is an @@ -238,12 +239,24 @@ module _ #### `Id : A → (A → 𝒰)` is an embedding ```agda -module _ - {l : Level} (A : UU l) - where +is-emb-Id : {l : Level} (A : UU l) → is-emb (Id {A = A}) +is-emb-Id = is-emb-Id-preunivalence-axiom preunivalence +``` + +### Characteriation of equality of `Id` - is-emb-Id : is-emb (Id {A = A}) - is-emb-Id = is-emb-Id-preunivalence-axiom preunivalence A +```agda +equiv-Id : + {l : Level} {A : UU l} (a x : A) → (Id a ＝ Id x) ≃ (a ＝ x) +equiv-Id a x = + ( equiv-ev-refl x) ∘e + ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a)) ∘e + ( equiv-Π-equiv-family (λ _ → equiv-univalence)) ∘e + ( equiv-funext) ∘e + ( equiv-inv (Id a) (Id x)) + +equiv-fiber-Id : {l : Level} {A : UU l} (a : A) → fiber' Id (Id a) ≃ Σ A (Id a) +equiv-fiber-Id a = equiv-tot (equiv-Id a) ``` #### For any type family `B` over `A`, the type of pairs `(a , e)` consisting of `a : A` and a family of equivalences `e : (x : A) → (a ＝ x) ≃ B x` is a proposition @@ -324,7 +337,7 @@ It was first observed and proved by Evan Cavallo that preunivalence, or Axiom L, is sufficient to deduce that `Id : A → (A → 𝒰)` is an embedding. It was later observed and formalized by Martín Escardó that assuming the map `equiv-eq : (X ＝ Y) → (X ≃ Y)` is injective is enough. {{#cite TypeTopology}} -Martín Escardó formalizations can be found here: +Martín Escardó's formalizations can be found here: [https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html](https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html). {{#bibliography}} {{#reference TypeTopology}} {{#reference Esc17YetAnother}} diff --git a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md index 51dfe0ed13..b2397aee3c 100644 --- a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md +++ b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md @@ -167,14 +167,14 @@ module _ Given a map `a : I → A`, and a homotopy `H : f ~ g`, where `f, g : J → I`, we know that there is an identification `a ∘ f ＝ a ∘ g`. Transporting along this identification in the type of lifts of families of elements into a type family -`B : A → 𝓤`, we get a map +`B : A → 𝒰`, we get a map ```text ((j : J) → B (a (f j))) → ((j : J) → B (a (g j))) . ``` We show that this map is homotopic to transporting along `H` in the type family -`B ∘ a : I → 𝓤`. +`B ∘ a : I → 𝒰`. ```agda module _ diff --git a/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md index c197c952bc..8b53882043 100644 --- a/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md +++ b/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md @@ -33,7 +33,7 @@ open import orthogonal-factorization-systems.lifts-families-of-elements ## Idea -Consider a type family `B : A → 𝓤` and a map `a : I → A`. Then, given a map +Consider a type family `B : A → 𝒰` and a map `a : I → A`. Then, given a map `f : J → I`, we may pull back a [lift](orthogonal-factorization-systems.lifts-families-of-elements.md) of `a` to a lift of `a ∘ f`. diff --git a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md index d7951a5d85..552c91b146 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md @@ -45,7 +45,7 @@ given a coequalizer f ``` -with homotopy `H : e ∘ f ~ e ∘ g`, and a type family `P : X → 𝓤` over `X`, the +with homotopy `H : e ∘ f ~ e ∘ g`, and a type family `P : X → 𝒰` over `X`, the cofork ```text From 70929fded45c9828eec9b1d5f9fd7068761193c8 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Jan 2025 00:51:56 +0100 Subject: [PATCH 20/23] edits --- .../structured-equality-duality.lagda.md | 55 ++++++++++--------- 1 file changed, 28 insertions(+), 27 deletions(-) diff --git a/src/foundation/structured-equality-duality.lagda.md b/src/foundation/structured-equality-duality.lagda.md index 88ef8a17bd..c5ae5649e5 100644 --- a/src/foundation/structured-equality-duality.lagda.md +++ b/src/foundation/structured-equality-duality.lagda.md @@ -29,10 +29,14 @@ type family `B : A → 𝒰` there is a [mutual correspondence](foundation.logical-equivalences.md) between the following: -1. `𝒫`-structured binary families of maps `f : (y : A) → (x ＝ y) → B y`. +1. `𝒫`-structured families of maps `f : (y : A) → (x ＝ y) → B y` for every + `x : A`. 2. `𝒫`-structures on the equality of `Σ A B`. -Note that, by [univalence axiom](foundation.univalence.md), every structure +We refer to this as +{{#concept "structured equality duality" Agda=structured-equality-duality}}. + +**Note.** by [univalence axiom](foundation.univalence.md), every structure [transfers along equivalences](foundation.transport-along-equivalences.md). However, we maintain this as an assumption, since for most common notions of structure this property is independent of the univalence axiom. @@ -87,31 +91,28 @@ module _ {A : UU l1} {B : A → UU l2} where - abstract - forward-implication-subuniverse-equality-duality : - ( (x : A) (f : (y : A) → (x ＝ y) → B y) - (y : A) → is-in-subuniverse-map 𝒫 (f y)) → - is-separated 𝒫 (Σ A B) - forward-implication-subuniverse-equality-duality = - forward-implication-structured-equality-duality - ( is-in-subuniverse-equiv 𝒫) - - abstract - backward-implication-subuniverse-equality-duality : - is-separated 𝒫 (Σ A B) → - ( (x : A) (f : (y : A) → (x ＝ y) → B y) - (y : A) → is-in-subuniverse-map 𝒫 (f y)) - backward-implication-subuniverse-equality-duality = - backward-implication-structured-equality-duality - ( is-in-subuniverse-equiv 𝒫) - - abstract - subuniverse-equality-duality : - ( (x : A) (f : (y : A) → (x ＝ y) → B y) - (y : A) → is-in-subuniverse-map 𝒫 (f y)) ↔ - is-separated 𝒫 (Σ A B) - subuniverse-equality-duality = - structured-equality-duality (is-in-subuniverse-equiv 𝒫) + forward-implication-subuniverse-equality-duality : + ( (x : A) (f : (y : A) → (x ＝ y) → B y) + (y : A) → is-in-subuniverse-map 𝒫 (f y)) → + is-separated 𝒫 (Σ A B) + forward-implication-subuniverse-equality-duality = + forward-implication-structured-equality-duality + ( is-in-subuniverse-equiv 𝒫) + + backward-implication-subuniverse-equality-duality : + is-separated 𝒫 (Σ A B) → + ( (x : A) (f : (y : A) → (x ＝ y) → B y) + (y : A) → is-in-subuniverse-map 𝒫 (f y)) + backward-implication-subuniverse-equality-duality = + backward-implication-structured-equality-duality + ( is-in-subuniverse-equiv 𝒫) + + subuniverse-equality-duality : + ( (x : A) (f : (y : A) → (x ＝ y) → B y) + (y : A) → is-in-subuniverse-map 𝒫 (f y)) ↔ + is-separated 𝒫 (Σ A B) + subuniverse-equality-duality = + structured-equality-duality (is-in-subuniverse-equiv 𝒫) ``` ## See also From 2e284cee21f7c2180dd433b99ec2143468d3f018 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Jan 2025 01:01:45 +0100 Subject: [PATCH 21/23] more edits --- src/foundation/strong-preunivalence.lagda.md | 9 +++++---- src/foundation/structured-equality-duality.lagda.md | 11 ++++++----- 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/foundation/strong-preunivalence.lagda.md b/src/foundation/strong-preunivalence.lagda.md index d0a32feb13..ac56a91a6a 100644 --- a/src/foundation/strong-preunivalence.lagda.md +++ b/src/foundation/strong-preunivalence.lagda.md @@ -49,10 +49,11 @@ preunivalence axiom asserts that the particular family of maps `refl ↦ id-equiv` is a family of embeddings. While the strong preunivalence axiom is a strengthening of the preunivalence -axiom, it is still common generalization of the +axiom, it is still a common generalization of the [univalence axiom](foundation.univalence.md) and [axiom K](foundation-core.sets.md): if we assume the univalence axiom then -`is-small` is a proposition, and if we assume axiom K then every type is a set. +`is-small 𝒱 X` is a proposition, and if we assume axiom K then every type is a +set. ## Definitions @@ -95,8 +96,8 @@ preunivalence-axiom-strong-preunivalence-axiom L X = ### The strong preunivalence axiom generalizes axiom K -To show that preunivalence generalizes axiom K, we assume axiom K for the types -in question and for the universe itself. +To show that preunivalence generalizes axiom K, we assume axiom K for types of +equivalences and for the universe itself. ```agda instance-strong-preunivalence-instance-axiom-K : diff --git a/src/foundation/structured-equality-duality.lagda.md b/src/foundation/structured-equality-duality.lagda.md index c5ae5649e5..7fd9c3930b 100644 --- a/src/foundation/structured-equality-duality.lagda.md +++ b/src/foundation/structured-equality-duality.lagda.md @@ -36,12 +36,14 @@ following: We refer to this as {{#concept "structured equality duality" Agda=structured-equality-duality}}. -**Note.** by [univalence axiom](foundation.univalence.md), every structure +**Note.** by [the univalence axiom](foundation.univalence.md), every structure [transfers along equivalences](foundation.transport-along-equivalences.md). However, we maintain this as an assumption, since for most common notions of structure this property is independent of the univalence axiom. -## Construction +## Duality + +### Structured equality duality ```agda module _ @@ -75,11 +77,10 @@ module _ backward-implication-structured-equality-duality) ``` -## Corollaries - ### Subuniverse equality duality -Given a subuniverse `𝒫` then the following are logically equivalent: +Given a [subuniverse](foundation.subuniverses.m) `𝒫` then the following are +logically equivalent: 1. For every `x : A`, every family of maps `f : (y : A) → (x ＝ y) → B y` is a family of `𝒫`-maps. From d70578857b363d3ec63b55d02b55949a5e950d87 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Jan 2025 13:58:55 +0100 Subject: [PATCH 22/23] fix link --- src/foundation/universal-property-identity-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md index a970aa460e..1412af1bae 100644 --- a/src/foundation/universal-property-identity-types.lagda.md +++ b/src/foundation/universal-property-identity-types.lagda.md @@ -38,7 +38,7 @@ open import foundation-core.torsorial-type-families ## Idea -The {{#concept "universal property of identity types" Agda=equiv-eq-refl}} +The {{#concept "universal property of identity types" Agda=equiv-ev-refl}} characterizes families of maps out of the [identity type](foundation-core.identity-types.md). This universal property is also known as the **type theoretic Yoneda lemma**. From daee207275ebaa8e51bb682626481246f04c2187 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Jan 2025 17:48:58 +0100 Subject: [PATCH 23/23] transfer along equivalences --- src/foundation/structured-equality-duality.lagda.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/foundation/structured-equality-duality.lagda.md b/src/foundation/structured-equality-duality.lagda.md index 7fd9c3930b..463afb643d 100644 --- a/src/foundation/structured-equality-duality.lagda.md +++ b/src/foundation/structured-equality-duality.lagda.md @@ -24,8 +24,14 @@ open import foundation-core.equivalences ## Idea Given a [structure](foundation.structure.md) `𝒫` on types that transfers along -[equivalences](foundation-core.equivalences.md), then for every type `A` and -type family `B : A → 𝒰` there is a +[equivalences](foundation-core.equivalences.md) in the sense that `𝒫` comes +equipped with a family of maps + +```text + {X Y : 𝒰} → (X ≃ Y) → 𝒫 X → 𝒫 Y, +``` + +then for every type `A` and type family `B : A → 𝒰` there is a [mutual correspondence](foundation.logical-equivalences.md) between the following: @@ -79,7 +85,7 @@ module _ ### Subuniverse equality duality -Given a [subuniverse](foundation.subuniverses.m) `𝒫` then the following are +Given a [subuniverse](foundation.subuniverses.md) `𝒫` then the following are logically equivalent: 1. For every `x : A`, every family of maps `f : (y : A) → (x ＝ y) → B y` is a