Type arithmetic with the unit type

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

Created on 2022-01-27.
Last modified on 2024-02-06.

module foundation.type-arithmetic-unit-type where
Imports
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.unit-type
open import foundation.universe-levels

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

Idea

We prove arithmetical laws involving the unit type

Laws

Left unit law for dependent pair types

module _
  {l : Level} (A : unit  UU l)
  where

  map-left-unit-law-Σ : Σ unit A  A star
  map-left-unit-law-Σ (pair star a) = a

  map-inv-left-unit-law-Σ : A star  Σ unit A
  pr1 (map-inv-left-unit-law-Σ a) = star
  pr2 (map-inv-left-unit-law-Σ a) = a

  is-section-map-inv-left-unit-law-Σ :
    ( map-left-unit-law-Σ  map-inv-left-unit-law-Σ) ~ id
  is-section-map-inv-left-unit-law-Σ a = refl

  is-retraction-map-inv-left-unit-law-Σ :
    ( map-inv-left-unit-law-Σ  map-left-unit-law-Σ) ~ id
  is-retraction-map-inv-left-unit-law-Σ (pair star a) = refl

  is-equiv-map-left-unit-law-Σ : is-equiv map-left-unit-law-Σ
  is-equiv-map-left-unit-law-Σ =
    is-equiv-is-invertible
      map-inv-left-unit-law-Σ
      is-section-map-inv-left-unit-law-Σ
      is-retraction-map-inv-left-unit-law-Σ

  left-unit-law-Σ : Σ unit A  A star
  pr1 left-unit-law-Σ = map-left-unit-law-Σ
  pr2 left-unit-law-Σ = is-equiv-map-left-unit-law-Σ

  is-equiv-map-inv-left-unit-law-Σ : is-equiv map-inv-left-unit-law-Σ
  is-equiv-map-inv-left-unit-law-Σ =
    is-equiv-is-invertible
      map-left-unit-law-Σ
      is-retraction-map-inv-left-unit-law-Σ
      is-section-map-inv-left-unit-law-Σ

  inv-left-unit-law-Σ : A star  Σ unit A
  pr1 inv-left-unit-law-Σ = map-inv-left-unit-law-Σ
  pr2 inv-left-unit-law-Σ = is-equiv-map-inv-left-unit-law-Σ

Left unit law for cartesian products

module _
  {l : Level} {A : UU l}
  where

  map-left-unit-law-product : unit × A  A
  map-left-unit-law-product = pr2

  map-inv-left-unit-law-product : A  unit × A
  map-inv-left-unit-law-product = map-inv-left-unit-law-Σ  x  A)

  is-section-map-inv-left-unit-law-product :
    ( map-left-unit-law-product  map-inv-left-unit-law-product) ~ id
  is-section-map-inv-left-unit-law-product =
    is-section-map-inv-left-unit-law-Σ  x  A)

  is-retraction-map-inv-left-unit-law-product :
    ( map-inv-left-unit-law-product  map-left-unit-law-product) ~ id
  is-retraction-map-inv-left-unit-law-product (pair star a) = refl

  is-equiv-map-left-unit-law-product : is-equiv map-left-unit-law-product
  is-equiv-map-left-unit-law-product =
    is-equiv-is-invertible
      map-inv-left-unit-law-product
      is-section-map-inv-left-unit-law-product
      is-retraction-map-inv-left-unit-law-product

  left-unit-law-product : (unit × A)  A
  pr1 left-unit-law-product = map-left-unit-law-product
  pr2 left-unit-law-product = is-equiv-map-left-unit-law-product

  is-equiv-map-inv-left-unit-law-product :
    is-equiv map-inv-left-unit-law-product
  is-equiv-map-inv-left-unit-law-product =
    is-equiv-is-invertible
      map-left-unit-law-product
      is-retraction-map-inv-left-unit-law-product
      is-section-map-inv-left-unit-law-product

  inv-left-unit-law-product : A  (unit × A)
  pr1 inv-left-unit-law-product = map-inv-left-unit-law-product
  pr2 inv-left-unit-law-product = is-equiv-map-inv-left-unit-law-product

Right unit law for cartesian products

  map-right-unit-law-product : A × unit  A
  map-right-unit-law-product = pr1

  map-inv-right-unit-law-product : A  A × unit
  pr1 (map-inv-right-unit-law-product a) = a
  pr2 (map-inv-right-unit-law-product a) = star

  is-section-map-inv-right-unit-law-product :
    (map-right-unit-law-product  map-inv-right-unit-law-product) ~ id
  is-section-map-inv-right-unit-law-product a = refl

  is-retraction-map-inv-right-unit-law-product :
    (map-inv-right-unit-law-product  map-right-unit-law-product) ~ id
  is-retraction-map-inv-right-unit-law-product (pair a star) = refl

  is-equiv-map-right-unit-law-product : is-equiv map-right-unit-law-product
  is-equiv-map-right-unit-law-product =
    is-equiv-is-invertible
      map-inv-right-unit-law-product
      is-section-map-inv-right-unit-law-product
      is-retraction-map-inv-right-unit-law-product

  right-unit-law-product : (A × unit)  A
  pr1 right-unit-law-product = map-right-unit-law-product
  pr2 right-unit-law-product = is-equiv-map-right-unit-law-product

Left unit law for dependent function types

module _
  {l : Level} (A : unit  UU l)
  where

  map-left-unit-law-Π : ((t : unit)  A t)  A star
  map-left-unit-law-Π f = f star

  map-inv-left-unit-law-Π : A star  ((t : unit)  A t)
  map-inv-left-unit-law-Π a star = a

  is-section-map-inv-left-unit-law-Π :
    ( map-left-unit-law-Π  map-inv-left-unit-law-Π) ~ id
  is-section-map-inv-left-unit-law-Π a = refl

  is-retraction-map-inv-left-unit-law-Π :
    ( map-inv-left-unit-law-Π  map-left-unit-law-Π) ~ id
  is-retraction-map-inv-left-unit-law-Π f = eq-htpy  star  refl)

  is-equiv-map-left-unit-law-Π : is-equiv map-left-unit-law-Π
  is-equiv-map-left-unit-law-Π =
    is-equiv-is-invertible
      map-inv-left-unit-law-Π
      is-section-map-inv-left-unit-law-Π
      is-retraction-map-inv-left-unit-law-Π

  left-unit-law-Π : ((t : unit)  A t)  A star
  pr1 left-unit-law-Π = map-left-unit-law-Π
  pr2 left-unit-law-Π = is-equiv-map-left-unit-law-Π

  is-equiv-map-inv-left-unit-law-Π : is-equiv map-inv-left-unit-law-Π
  is-equiv-map-inv-left-unit-law-Π =
    is-equiv-is-invertible
      map-left-unit-law-Π
      is-retraction-map-inv-left-unit-law-Π
      is-section-map-inv-left-unit-law-Π

  inv-left-unit-law-Π : A star  ((t : unit)  A t)
  pr1 inv-left-unit-law-Π = map-inv-left-unit-law-Π
  pr2 inv-left-unit-law-Π = is-equiv-map-inv-left-unit-law-Π

Left unit law for nondependent function types

module _
  {l : Level} (A : UU l)
  where

  map-left-unit-law-function-type : (unit  A)  A
  map-left-unit-law-function-type = map-left-unit-law-Π  _  A)

  map-inv-left-unit-law-function-type : A  (unit  A)
  map-inv-left-unit-law-function-type = map-inv-left-unit-law-Π  _  A)

  is-equiv-map-left-unit-law-function-type :
    is-equiv map-left-unit-law-function-type
  is-equiv-map-left-unit-law-function-type =
    is-equiv-map-left-unit-law-Π λ _  A

  is-equiv-map-inv-left-unit-law-function-type :
    is-equiv map-inv-left-unit-law-function-type
  is-equiv-map-inv-left-unit-law-function-type =
    is-equiv-map-inv-left-unit-law-Π λ _  A

  left-unit-law-function-type : (unit  A)  A
  left-unit-law-function-type = left-unit-law-Π  _  A)

  inv-left-unit-law-function-type : A  (unit  A)
  inv-left-unit-law-function-type = inv-left-unit-law-Π  _  A)

See also

  • That unit is the terminal type is a corollary of is-contr-Π, which may be found in foundation-core.contractible-types. This can be considered a right zero law for function types ((A → unit) ≃ unit).

Recent changes