Type arithmetic for cartesian product types

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

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

module foundation.type-arithmetic-cartesian-product-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.type-arithmetic-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.propositions

Idea

We prove laws for the manipulation of cartesian products with respect to themselves and dependent pair types.

Laws

Commutativity of cartesian products

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

  map-commutative-product : A × B → B × A
  pr1 (map-commutative-product (pair a b)) = b
  pr2 (map-commutative-product (pair a b)) = a

  map-inv-commutative-product : B × A → A × B
  pr1 (map-inv-commutative-product (pair b a)) = a
  pr2 (map-inv-commutative-product (pair b a)) = b

  is-section-map-inv-commutative-product :
    (map-commutative-product ∘ map-inv-commutative-product) ~ id
  is-section-map-inv-commutative-product (pair b a) = refl

  is-retraction-map-inv-commutative-product :
    (map-inv-commutative-product ∘ map-commutative-product) ~ id
  is-retraction-map-inv-commutative-product (pair a b) = refl

  is-equiv-map-commutative-product : is-equiv map-commutative-product
  is-equiv-map-commutative-product =
    is-equiv-is-invertible
      map-inv-commutative-product
      is-section-map-inv-commutative-product
      is-retraction-map-inv-commutative-product

  commutative-product : (A × B) ≃ (B × A)
  pr1 commutative-product = map-commutative-product
  pr2 commutative-product = is-equiv-map-commutative-product

Associativity of cartesian products

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

  map-associative-product : (A × B) × C → A × (B × C)
  map-associative-product = map-associative-Σ A (λ _ → B) (λ _ → C)

  map-inv-associative-product : A × (B × C) → (A × B) × C
  map-inv-associative-product = map-inv-associative-Σ A (λ _ → B) (λ _ → C)

  is-section-map-inv-associative-product :
    (map-associative-product ∘ map-inv-associative-product) ~ id
  is-section-map-inv-associative-product =
    is-section-map-inv-associative-Σ A (λ _ → B) (λ _ → C)

  is-retraction-map-inv-associative-product :
    (map-inv-associative-product ∘ map-associative-product) ~ id
  is-retraction-map-inv-associative-product =
    is-retraction-map-inv-associative-Σ A (λ _ → B) (λ _ → C)

  is-equiv-map-associative-product : is-equiv map-associative-product
  is-equiv-map-associative-product =
    is-equiv-map-associative-Σ A (λ _ → B) (λ _ → C)

  associative-product : ((A × B) × C) ≃ (A × (B × C))
  associative-product = associative-Σ A (λ _ → B) (λ _ → C)

The unit laws of cartesian product types with respect to contractible types

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

  right-unit-law-product-is-contr : A × B ≃ A
  right-unit-law-product-is-contr = right-unit-law-Σ-is-contr (λ _ → is-contr-B)

  inv-right-unit-law-product-is-contr : A ≃ A × B
  inv-right-unit-law-product-is-contr =
    inv-equiv right-unit-law-product-is-contr

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

  left-unit-law-product-is-contr : A × B ≃ B
  left-unit-law-product-is-contr =
    left-unit-law-Σ-is-contr is-contr-A (center is-contr-A)

  inv-left-unit-law-product-is-contr : B ≃ A × B
  inv-left-unit-law-product-is-contr = inv-equiv left-unit-law-product-is-contr

  is-equiv-pr2-product-is-contr : is-equiv (pr2 {B = λ _ → B})
  is-equiv-pr2-product-is-contr =
    is-equiv-comp
      ( pr1)
      ( map-commutative-product)
      ( is-equiv-map-commutative-product)
      ( is-equiv-pr1-is-contr (λ _ → is-contr-A))

  equiv-pr2-product-is-contr : (A × B) ≃ B
  pr1 equiv-pr2-product-is-contr = pr2
  pr2 equiv-pr2-product-is-contr = is-equiv-pr2-product-is-contr

Adding redundant properties

equiv-add-redundant-prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  is-prop B → (f : A → B) → A ≃ A × B
pr1 (equiv-add-redundant-prop is-prop-B f) a = a , f a
pr2 (equiv-add-redundant-prop is-prop-B f) =
  is-equiv-is-invertible
    ( pr1)
    ( λ p → eq-pair refl (eq-is-prop is-prop-B))
    ( refl-htpy)

See also

Recent changes