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