The universal properties of cartesian product types

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

Created on 2022-02-10.
Last modified on 2024-04-11.

module foundation.universal-property-cartesian-product-types where
Imports 
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.standard-pullbacks
open import foundation.unit-type
open import foundation.universal-property-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-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.pullbacks
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.universal-property-pullbacks

Idea

Cartesian products have universal properties both as limits and as colimits of types. The universal property of cartesian products as limits states that, given types A, B and X, maps into the cartesian product X → A × B are in correspondence with pairs of maps X → A and X → B. The universal property of cartesian products as colimits states that maps out of the cartesian product A × B → X are in correspondence with "curried" maps A → B → X.

Observe that the universal property of cartesian products as limits can be understood as a categorified version of the familiar distributivity of exponents over products

while the universal property of cartesian products as colimits are a categorified version of the identity

Theorems

The universal property of cartesian products as limits

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : X → UU l2} {B : X → UU l3}
  where

  map-up-product :
    ((x : X) → A x × B x) → ((x : X) → A x) × ((x : X) → B x)
  pr1 (map-up-product f) x = pr1 (f x)
  pr2 (map-up-product f) x = pr2 (f x)

  map-inv-up-product :
    (((x : X) → A x) × ((x : X) → B x)) → (x : X) → A x × B x
  pr1 (map-inv-up-product (f , g) x) = f x
  pr2 (map-inv-up-product (f , g) x) = g x

  iff-up-product :
    ((x : X) → A x × B x) ↔ ((x : X) → A x) × ((x : X) → B x)
  iff-up-product = (map-up-product , map-inv-up-product)

  up-product : is-equiv map-up-product
  up-product =
    is-equiv-is-invertible (map-inv-up-product) (refl-htpy) (refl-htpy)

  is-equiv-map-inv-up-product : is-equiv map-inv-up-product
  is-equiv-map-inv-up-product = is-equiv-map-inv-is-equiv up-product

  equiv-up-product :
    ((x : X) → A x × B x) ≃ (((x : X) → A x) × ((x : X) → B x))
  pr1 equiv-up-product = map-up-product
  pr2 equiv-up-product = up-product

  inv-equiv-up-product :
    (((x : X) → A x) × ((x : X) → B x)) ≃ ((x : X) → A x × B x)
  inv-equiv-up-product = inv-equiv equiv-up-product

The universal property of cartesian products as pullbacks

A different way to state the universal property of cartesian products as limits is to say that the canonical cone over the terminal type unit

           pr2
   A × B ------> B
     |           |
 pr1 |           |
     ∨           ∨
     A -------> unit

is a pullback. The universal property of pullbacks states in this case that maps into A × B are in correspondence with pairs of maps into A and B such that the square

     X --------> B
     |           |
     |           |
     ∨           ∨
     A -------> unit

commutes. However, all parallel maps into the terminal type are equal, hence the coherence requirement is redundant.

We start by constructing the cone for two maps into the unit type.

module _
  {l1 l2 : Level} (A : UU l1) (B : UU l2)
  where

  cone-cartesian-product : cone (terminal-map A) (terminal-map B) (A × B)
  pr1 cone-cartesian-product = pr1
  pr1 (pr2 cone-cartesian-product) = pr2
  pr2 (pr2 cone-cartesian-product) = refl-htpy

Next, we show that cartesian products are a special case of pullbacks.

  gap-cartesian-product :
    A × B → standard-pullback (terminal-map A) (terminal-map B)
  gap-cartesian-product =
    gap (terminal-map A) (terminal-map B) cone-cartesian-product

  inv-gap-cartesian-product :
    standard-pullback (terminal-map A) (terminal-map B) → A × B
  pr1 (inv-gap-cartesian-product (a , b , p)) = a
  pr2 (inv-gap-cartesian-product (a , b , p)) = b

  abstract
    is-section-inv-gap-cartesian-product :
      is-section gap-cartesian-product inv-gap-cartesian-product
    is-section-inv-gap-cartesian-product (a , b , p) =
      map-extensionality-standard-pullback
        ( terminal-map A)
        ( terminal-map B)
        ( refl)
        ( refl)
        ( eq-is-contr (is-prop-unit star star))

  is-retraction-inv-gap-cartesian-product :
    is-retraction gap-cartesian-product inv-gap-cartesian-product
  is-retraction-inv-gap-cartesian-product (a , b) = refl

  abstract
    is-pullback-cartesian-product :
      is-pullback (terminal-map A) (terminal-map B) cone-cartesian-product
    is-pullback-cartesian-product =
      is-equiv-is-invertible
        inv-gap-cartesian-product
        is-section-inv-gap-cartesian-product
        is-retraction-inv-gap-cartesian-product

We conclude that cartesian products satisfy the universal property of pullbacks.

  abstract
    universal-property-pullback-cartesian-product :
      universal-property-pullback
        ( terminal-map A)
        ( terminal-map B)
        ( cone-cartesian-product)
    universal-property-pullback-cartesian-product =
      universal-property-pullback-is-pullback
        ( terminal-map A)
        ( terminal-map B)
        ( cone-cartesian-product)
        ( is-pullback-cartesian-product)

The universal property of cartesian products as colimits

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

  equiv-ind-product : ((x : A) (y : B) → C (x , y)) ≃ ((t : A × B) → C t)
  equiv-ind-product = equiv-ind-Σ

Recent changes