# The type theoretic principle of choice

Content created by Egbert Rijke.

Created on 2023-11-24.

module foundation-core.type-theoretic-principle-of-choice where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types


## 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.

We establish this equivalence both for explicit and implicit function types.

## Definitions

### Dependent products of dependent pair types

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
(C : (x : A) → B x → UU l3)
where

Π-total-fam : UU (l1 ⊔ l2 ⊔ l3)
Π-total-fam = (x : A) → Σ (B x) (C x)

universally-structured-Π : UU (l1 ⊔ l2 ⊔ l3)
universally-structured-Π = Σ ((x : A) → B x) (λ f → (x : A) → C x (f x))


### Implicit dependent products of dependent pair types

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
(C : (x : A) → B x → UU l3)
where

implicit-Π-total-fam : UU (l1 ⊔ l2 ⊔ l3)
implicit-Π-total-fam = {x : A} → Σ (B x) (C x)

universally-structured-implicit-Π : UU (l1 ⊔ l2 ⊔ l3)
universally-structured-implicit-Π =
Σ ({x : A} → B x) (λ f → {x : A} → C x (f {x}))


## Theorem

### The distributivity of Π over Σ

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
where

map-distributive-Π-Σ : Π-total-fam C → universally-structured-Π C
pr1 (map-distributive-Π-Σ φ) x = pr1 (φ x)
pr2 (map-distributive-Π-Σ φ) x = pr2 (φ x)

map-inv-distributive-Π-Σ : universally-structured-Π C → Π-total-fam C
pr1 (map-inv-distributive-Π-Σ ψ x) = (pr1 ψ) x
pr2 (map-inv-distributive-Π-Σ ψ x) = (pr2 ψ) x

is-section-map-inv-distributive-Π-Σ :
map-distributive-Π-Σ ∘ map-inv-distributive-Π-Σ ~ id
is-section-map-inv-distributive-Π-Σ (ψ , ψ') = refl

is-retraction-map-inv-distributive-Π-Σ :
map-inv-distributive-Π-Σ ∘ map-distributive-Π-Σ ~ id
is-retraction-map-inv-distributive-Π-Σ φ = refl

abstract
is-equiv-map-distributive-Π-Σ : is-equiv (map-distributive-Π-Σ)
is-equiv-map-distributive-Π-Σ =
is-equiv-is-invertible
( map-inv-distributive-Π-Σ)
( is-section-map-inv-distributive-Π-Σ)
( is-retraction-map-inv-distributive-Π-Σ)

distributive-Π-Σ : Π-total-fam C ≃ universally-structured-Π C
pr1 distributive-Π-Σ = map-distributive-Π-Σ
pr2 distributive-Π-Σ = is-equiv-map-distributive-Π-Σ

abstract
is-equiv-map-inv-distributive-Π-Σ : is-equiv (map-inv-distributive-Π-Σ)
is-equiv-map-inv-distributive-Π-Σ =
is-equiv-is-invertible
( map-distributive-Π-Σ)
( is-retraction-map-inv-distributive-Π-Σ)
( is-section-map-inv-distributive-Π-Σ)

inv-distributive-Π-Σ : universally-structured-Π C ≃ Π-total-fam C
pr1 inv-distributive-Π-Σ = map-inv-distributive-Π-Σ
pr2 inv-distributive-Π-Σ = is-equiv-map-inv-distributive-Π-Σ


### The distributivity of implicit Π over Σ

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
where

map-distributive-implicit-Π-Σ :
implicit-Π-total-fam C → universally-structured-implicit-Π C
pr1 (map-distributive-implicit-Π-Σ φ) {x} = pr1 (φ {x})
pr2 (map-distributive-implicit-Π-Σ φ) {x} = pr2 (φ {x})

map-inv-distributive-implicit-Π-Σ :
universally-structured-implicit-Π C → implicit-Π-total-fam C
pr1 (map-inv-distributive-implicit-Π-Σ ψ {x}) = pr1 ψ
pr2 (map-inv-distributive-implicit-Π-Σ ψ {x}) = pr2 ψ

is-section-map-inv-distributive-implicit-Π-Σ :
( ( map-distributive-implicit-Π-Σ) ∘
( map-inv-distributive-implicit-Π-Σ)) ~ id
is-section-map-inv-distributive-implicit-Π-Σ (ψ , ψ') = refl

is-retraction-map-inv-distributive-implicit-Π-Σ :
( ( map-inv-distributive-implicit-Π-Σ) ∘
( map-distributive-implicit-Π-Σ)) ~ id
is-retraction-map-inv-distributive-implicit-Π-Σ φ = refl

abstract
is-equiv-map-distributive-implicit-Π-Σ :
is-equiv (map-distributive-implicit-Π-Σ)
is-equiv-map-distributive-implicit-Π-Σ =
is-equiv-is-invertible
( map-inv-distributive-implicit-Π-Σ)
( is-section-map-inv-distributive-implicit-Π-Σ)
( is-retraction-map-inv-distributive-implicit-Π-Σ)

distributive-implicit-Π-Σ :
implicit-Π-total-fam C ≃ universally-structured-implicit-Π C
pr1 distributive-implicit-Π-Σ = map-distributive-implicit-Π-Σ
pr2 distributive-implicit-Π-Σ = is-equiv-map-distributive-implicit-Π-Σ

abstract
is-equiv-map-inv-distributive-implicit-Π-Σ :
is-equiv (map-inv-distributive-implicit-Π-Σ)
is-equiv-map-inv-distributive-implicit-Π-Σ =
is-equiv-is-invertible
( map-distributive-implicit-Π-Σ)
( is-retraction-map-inv-distributive-implicit-Π-Σ)
( is-section-map-inv-distributive-implicit-Π-Σ)

inv-distributive-implicit-Π-Σ :
(universally-structured-implicit-Π C) ≃ (implicit-Π-total-fam C)
pr1 inv-distributive-implicit-Π-Σ = map-inv-distributive-implicit-Π-Σ
pr2 inv-distributive-implicit-Π-Σ = is-equiv-map-inv-distributive-implicit-Π-Σ


### Ordinary functions into a Σ-type

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : B → UU l3}
where

mapping-into-Σ : (A → Σ B C) → Σ (A → B) (λ f → (x : A) → C (f x))
mapping-into-Σ = map-distributive-Π-Σ {B = λ _ → B}

abstract
is-equiv-mapping-into-Σ : is-equiv mapping-into-Σ
is-equiv-mapping-into-Σ = is-equiv-map-distributive-Π-Σ

equiv-mapping-into-Σ :
(A → Σ B C) ≃ Σ (A → B) (λ f → (x : A) → C (f x))
pr1 equiv-mapping-into-Σ = mapping-into-Σ
pr2 equiv-mapping-into-Σ = is-equiv-mapping-into-Σ