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


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.


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)

  htpy-universally-structured-Π :
    (t t' : universally-structured-Π C)  UU (l1  l2  l3)
  htpy-universally-structured-Π t t' =
      ( λ (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) =
      ( λ {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)

  htpy-universally-structured-implicit-Π :
    (t t' : universally-structured-implicit-Π C)  UU (l1  l2  l3)
  htpy-universally-structured-implicit-Π t t' =
      ( λ (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) =
      ( λ {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')


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

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

  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