The universal property of coproduct types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-02-08.
Last modified on 2024-02-06.

module foundation.universal-property-coproduct-types where
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.function-extensionality
open import foundation.universal-property-equivalences
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.coproduct-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.precomposition-functions


The universal property and dependent universal property of coproduct types characterize maps and dependent functions out of coproduct types.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}

  ev-inl-inr :
    {l3 : Level} (P : A + B  UU l3) 
    ((t : A + B)  P t)  ((x : A)  P (inl x)) × ((y : B)  P (inr y))
  pr1 (ev-inl-inr P s) x = s (inl x)
  pr2 (ev-inl-inr P s) y = s (inr y)

  dependent-universal-property-coproduct :
    {l3 : Level} (P : A + B  UU l3)  is-equiv (ev-inl-inr P)
  dependent-universal-property-coproduct P =
      ( λ p  ind-coproduct P (pr1 p) (pr2 p))
      ( ind-Σ  f g  eq-pair refl refl))
      ( λ s  eq-htpy (ind-coproduct _ refl-htpy refl-htpy))

  equiv-dependent-universal-property-coproduct :
    {l3 : Level} (P : A + B  UU l3) 
    ((x : A + B)  P x)  (((a : A)  P (inl a)) × ((b : B)  P (inr b)))
  pr1 (equiv-dependent-universal-property-coproduct P) = ev-inl-inr P
  pr2 (equiv-dependent-universal-property-coproduct P) =
    dependent-universal-property-coproduct P

    universal-property-coproduct :
      {l3 : Level} (X : UU l3)  is-equiv (ev-inl-inr  _  X))
    universal-property-coproduct X =
      dependent-universal-property-coproduct  _  X)

  equiv-universal-property-coproduct :
    {l3 : Level} (X : UU l3)  (A + B  X)  ((A  X) × (B  X))
  equiv-universal-property-coproduct X =
    equiv-dependent-universal-property-coproduct  _  X)

    uniqueness-coproduct :
      {l3 : Level} {Y : UU l3} (i : A  Y) (j : B  Y) 
      ( {l : Level} (X : UU l) 
        is-equiv  (s : Y  X)  pair' (s  i) (s  j))) 
      is-equiv (rec-coproduct i j)
    uniqueness-coproduct i j H =
        ( rec-coproduct i j)
        ( λ X 
            ( ev-inl-inr  _  X))
            ( precomp (rec-coproduct i j) X)
            ( universal-property-coproduct X)
            ( H X))

    universal-property-coproduct-is-equiv-rec-coproduct :
      {l3 : Level} (X : UU l3) (i : A  X) (j : B  X) 
      is-equiv (rec-coproduct i j) 
      (l4 : Level) (Y : UU l4) 
      is-equiv  (s : X  Y)  pair' (s  i) (s  j))
    universal-property-coproduct-is-equiv-rec-coproduct X i j H l Y =
        ( ev-inl-inr  _  Y))
        ( precomp (rec-coproduct i j) Y)
        ( is-equiv-precomp-is-equiv
          ( rec-coproduct i j)
          ( H)
          ( Y))
        ( universal-property-coproduct Y)

Recent changes