The universal property of dependent pair types

module foundation.universal-property-dependent-pair-types where

open import foundation.function-extensionality

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

Idea

The universal property of dependent pair types gives us a characterization of maps out of a dependent pair types.

Theorem

abstract
  is-equiv-ev-pair :
    {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} →
    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))

equiv-ev-pair :
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} →
  ((x : Σ A B) → C x) ≃ ((a : A) (b : B a) → C (pair a b))
pr1 equiv-ev-pair = ev-pair
pr2 equiv-ev-pair = is-equiv-ev-pair