The type theoretic principle of choice

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified on 2023-11-24.

module foundation-core.type-theoretic-principle-of-choice where
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


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.


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)

  Π-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)

  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}))


The distributivity of Π over Σ

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

  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

    is-equiv-map-distributive-Π-Σ : is-equiv (map-distributive-Π-Σ)
    is-equiv-map-distributive-Π-Σ =
        ( 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-Π-Σ

    is-equiv-map-inv-distributive-Π-Σ : is-equiv (map-inv-distributive-Π-Σ)
    is-equiv-map-inv-distributive-Π-Σ =
        ( 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}

  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

    is-equiv-map-distributive-implicit-Π-Σ :
      is-equiv (map-distributive-implicit-Π-Σ)
    is-equiv-map-distributive-implicit-Π-Σ =
        ( 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-Π-Σ

    is-equiv-map-inv-distributive-implicit-Π-Σ :
      is-equiv (map-inv-distributive-implicit-Π-Σ)
    is-equiv-map-inv-distributive-implicit-Π-Σ =
        ( 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}

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

    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-Σ

Recent changes