The type theoretic principle of choice
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Vojtěch Štěpančík and Elisabeth Stenholm.
Created on 2022-06-01.
Last modified on 2024-02-06.
module foundation.type-theoretic-principle-of-choice where open import foundation-core.type-theoretic-principle-of-choice public
Imports
open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.implicit-function-types open import foundation.structure-identity-principle open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.transport-along-identifications
Idea
A dependent function taking values in a dependent pair type is equivalently described as a pair of dependent functions. This equivalence, which gives the distributivity of Π over Σ, is also known as the type theoretic principle of choice. Indeed, it is the Curry-Howard interpretation of (one formulation of) the axiom of choice.
In this file we record some further facts about the
structures introduced in
foundation-core.type-theoretic-principle-of-choice
.
We relate precomposition of maps into a dependent pair type by a function with
precomposition in dependent pair types of functions in the file
orthogonal-factorization-systems.precomposition-lifts-families-of-elements
.
Lemma
Characterizing the identity type of universally-structured-Π
module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) where htpy-universally-structured-Π : (t t' : universally-structured-Π C) → UU (l1 ⊔ l2 ⊔ l3) htpy-universally-structured-Π t t' = universally-structured-Π ( λ (x : A) (p : (pr1 t) x = (pr1 t') x) → tr (C x) p ((pr2 t) x) = (pr2 t') x) extensionality-universally-structured-Π : (t t' : universally-structured-Π C) → (t = t') ≃ htpy-universally-structured-Π t t' extensionality-universally-structured-Π (f , g) = extensionality-Σ ( λ {f'} g' (H : f ~ f') → (x : A) → tr (C x) (H x) (g x) = g' x) ( refl-htpy) ( refl-htpy) ( λ f' → equiv-funext) ( λ g' → equiv-funext) eq-htpy-universally-structured-Π : {t t' : universally-structured-Π C} → htpy-universally-structured-Π t t' → t = t' eq-htpy-universally-structured-Π {t} {t'} = map-inv-equiv (extensionality-universally-structured-Π t t')
Characterizing the identity type of universally-structured-implicit-Π
module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) where htpy-universally-structured-implicit-Π : (t t' : universally-structured-implicit-Π C) → UU (l1 ⊔ l2 ⊔ l3) htpy-universally-structured-implicit-Π t t' = universally-structured-Π ( λ (x : A) (p : (pr1 t) {x} = (pr1 t') {x}) → tr (C x) p ((pr2 t) {x}) = (pr2 t') {x}) extensionality-universally-structured-implicit-Π : (t t' : universally-structured-implicit-Π C) → (t = t') ≃ htpy-universally-structured-implicit-Π t t' extensionality-universally-structured-implicit-Π (f , g) = extensionality-Σ ( λ {f'} g' H → (x : A) → tr (C x) (H x) (g {x}) = g' {x}) ( refl-htpy) ( refl-htpy) ( λ f' → equiv-funext-implicit) ( λ g' → equiv-funext-implicit) eq-htpy-universally-structured-implicit-Π : {t t' : universally-structured-implicit-Π C} → htpy-universally-structured-implicit-Π t t' → t = t' eq-htpy-universally-structured-implicit-Π {t} {t'} = map-inv-equiv (extensionality-universally-structured-implicit-Π t t')
Corollaries
Characterizing the identity type of Π-total-fam
module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) (f g : (a : A) → Σ (B a) (C a)) where Eq-Π-total-fam : UU (l1 ⊔ l2 ⊔ l3) Eq-Π-total-fam = Π-total-fam (λ x (p : pr1 (f x) = pr1 (g x)) → tr (C x) p (pr2 (f x)) = pr2 (g x)) extensionality-Π-total-fam : (f = g) ≃ Eq-Π-total-fam extensionality-Π-total-fam = ( inv-distributive-Π-Σ) ∘e ( extensionality-universally-structured-Π C ( map-distributive-Π-Σ f) ( map-distributive-Π-Σ g)) ∘e ( equiv-ap distributive-Π-Σ f g) eq-Eq-Π-total-fam : Eq-Π-total-fam → f = g eq-Eq-Π-total-fam = map-inv-equiv extensionality-Π-total-fam
Characterizing the identity type of implicit-Π-total-fam
module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) (f g : {a : A} → Σ (B a) (C a)) where extensionality-implicit-Π-total-fam : (Id {A = {a : A} → Σ (B a) (C a)} f g) ≃ Eq-Π-total-fam C (λ x → f {x}) (λ x → g {x}) extensionality-implicit-Π-total-fam = ( extensionality-Π-total-fam C (λ x → f {x}) (λ x → g {x})) ∘e ( equiv-ap equiv-explicit-implicit-Π f g) eq-Eq-implicit-Π-total-fam : Eq-Π-total-fam C (λ x → f {x}) (λ x → g {x}) → (Id {A = {a : A} → Σ (B a) (C a)} f g) eq-Eq-implicit-Π-total-fam = map-inv-equiv extensionality-implicit-Π-total-fam
Recent changes
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2024-01-27. Vojtěch Štěpančík. Refactor properties of lifts of families out of 26-descent (#988).
- 2023-12-21. Fredrik Bakke. Action on homotopies of functions (#973).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-10-28. Fredrik Bakke and Vojtěch Štěpančík. Implicit function extensionality (#891).