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.

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-Σ