The universal property of dependent pair types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Vojtěch Štěpančík, Daniel Gratzer and Elisabeth Stenholm.

Created on 2022-01-31.
Last modified on 2024-03-02.

module foundation.universal-property-dependent-pair-types where
Imports
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types

Idea

The universal property of dependent pair types characterizes of maps out of dependent pair types. It states that uncurried maps (x : Σ A B) → C x are in correspondence with curried maps (a : A) (b : B a) → C (a , b).

Theorem

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

  abstract
    is-equiv-ev-pair : is-equiv (ev-pair {C = C})
    pr1 (pr1 is-equiv-ev-pair) = ind-Σ
    pr2 (pr1 is-equiv-ev-pair) = refl-htpy
    pr1 (pr2 is-equiv-ev-pair) = ind-Σ
    pr2 (pr2 is-equiv-ev-pair) f = eq-htpy (ind-Σ  x y  refl))

  abstract
    is-equiv-ind-Σ : is-equiv (ind-Σ {C = C})
    is-equiv-ind-Σ = is-equiv-is-section is-equiv-ev-pair refl-htpy

  equiv-ev-pair : ((x : Σ A B)  C x)  ((a : A) (b : B a)  C (a , b))
  pr1 equiv-ev-pair = ev-pair
  pr2 equiv-ev-pair = is-equiv-ev-pair

  equiv-ind-Σ : ((a : A) (b : B a)  C (a , b))  ((x : Σ A B)  C x)
  pr1 equiv-ind-Σ = ind-Σ
  pr2 equiv-ind-Σ = is-equiv-ind-Σ

Properties

Iterated currying

equiv-ev-pair² :
  { l1 l2 l3 l4 l5 l6 : Level}
  { A : UU l1} {B : A  UU l2} {C : UU l3}
  { X : UU l4} {Y : X  UU l5}
  { Z : ( Σ A B  C)  Σ X Y  UU l6} 
  Σ ( Σ A B  C)  k  ( xy : Σ X Y)  Z k xy) 
  Σ ( (a : A)  B a  C)  k  (x : X)  (y : Y x)  Z (ind-Σ k) (x , y))
equiv-ev-pair² {X = X} {Y = Y} {Z = Z} =
  equiv-Σ
    ( λ k  (x : X) (y : Y x)  Z (ind-Σ k) (x , y))
    ( equiv-ev-pair)
    ( λ k  equiv-ev-pair)

equiv-ev-pair³ :
  { l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level} 
  { A : UU l1} {B : A  UU l2} {C : UU l3}
  { X : UU l4} {Y : X  UU l5} {Z : UU l6}
  { U : UU l7} {V : U  UU l8}
  { W : ((Σ A B)  C)  ((Σ X Y)  Z)  (Σ U V)  UU l9} 
  Σ ( (Σ A B)  C)
    ( λ k 
      Σ ( (Σ X Y)  Z)
        ( λ l  ( uv : Σ U V)  W k l uv)) 
  Σ ( (a : A)  B a  C)
    ( λ k 
      Σ ( (x : X)  Y x  Z)
        ( λ l  (u : U)  (v : V u)  W (ind-Σ k) (ind-Σ l) (u , v)))
equiv-ev-pair³ {X = X} {Y = Y} {Z = Z} {U = U} {V = V} {W = W} =
  equiv-Σ
    ( λ k 
      Σ ( (x : X)  Y x  Z)
        ( λ l  (u : U)  (v : V u)  W (ind-Σ k) (ind-Σ l) (u , v)))
    ( equiv-ev-pair)
    ( λ k  equiv-ev-pair²)

Recent changes