# Type arithmetic with the empty type

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

Created on 2022-01-27.

module foundation.type-arithmetic-empty-type where

Imports
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.empty-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 empty type.

## Laws

### Left zero law for cartesian products

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

inv-pr1-product-empty : empty → empty × X
inv-pr1-product-empty ()

is-section-inv-pr1-product-empty : (pr1 ∘ inv-pr1-product-empty) ~ id
is-section-inv-pr1-product-empty ()

is-retraction-inv-pr1-product-empty : (inv-pr1-product-empty ∘ pr1) ~ id
is-retraction-inv-pr1-product-empty (pair () x)

is-equiv-pr1-product-empty : is-equiv (pr1 {A = empty} {B = λ t → X})
is-equiv-pr1-product-empty =
is-equiv-is-invertible
inv-pr1-product-empty
is-section-inv-pr1-product-empty
is-retraction-inv-pr1-product-empty

left-zero-law-product : (empty × X) ≃ empty
pr1 left-zero-law-product = pr1
pr2 left-zero-law-product = is-equiv-pr1-product-empty

module _
{l1 l2 : Level} (A : UU l1) (B : UU l2) (is-empty-A : is-empty A)
where
inv-pr1-product-is-empty : A → A × B
inv-pr1-product-is-empty a = ex-falso (is-empty-A a)

is-section-inv-pr1-product-is-empty : (pr1 ∘ inv-pr1-product-is-empty) ~ id
is-section-inv-pr1-product-is-empty a = ex-falso (is-empty-A a)

is-retraction-inv-pr1-product-is-empty : (inv-pr1-product-is-empty ∘ pr1) ~ id
is-retraction-inv-pr1-product-is-empty (pair a b) = ex-falso (is-empty-A a)

is-equiv-pr1-product-is-empty : is-equiv (pr1 {A = A} {B = λ a → B})
is-equiv-pr1-product-is-empty =
is-equiv-is-invertible
inv-pr1-product-is-empty
is-section-inv-pr1-product-is-empty
is-retraction-inv-pr1-product-is-empty

left-zero-law-product-is-empty : (A × B) ≃ A
pr1 left-zero-law-product-is-empty = pr1
pr2 left-zero-law-product-is-empty = is-equiv-pr1-product-is-empty


### Right zero law for cartesian products

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

inv-pr2-product-empty : empty → (X × empty)
inv-pr2-product-empty ()

is-section-inv-pr2-product-empty : (pr2 ∘ inv-pr2-product-empty) ~ id
is-section-inv-pr2-product-empty ()

is-retraction-inv-pr2-product-empty : (inv-pr2-product-empty ∘ pr2) ~ id
is-retraction-inv-pr2-product-empty (pair x ())

is-equiv-pr2-product-empty : is-equiv (pr2 {A = X} {B = λ x → empty})
is-equiv-pr2-product-empty =
is-equiv-is-invertible
inv-pr2-product-empty
is-section-inv-pr2-product-empty
is-retraction-inv-pr2-product-empty

right-zero-law-product : (X × empty) ≃ empty
pr1 right-zero-law-product = pr2
pr2 right-zero-law-product = is-equiv-pr2-product-empty

module _
{l1 l2 : Level} (A : UU l1) (B : UU l2) (is-empty-B : is-empty B)
where
inv-pr2-product-is-empty : B → A × B
inv-pr2-product-is-empty b = ex-falso (is-empty-B b)

is-section-inv-pr2-product-is-empty : (pr2 ∘ inv-pr2-product-is-empty) ~ id
is-section-inv-pr2-product-is-empty b = ex-falso (is-empty-B b)

is-retraction-inv-pr2-product-is-empty : (inv-pr2-product-is-empty ∘ pr2) ~ id
is-retraction-inv-pr2-product-is-empty (pair a b) = ex-falso (is-empty-B b)

is-equiv-pr2-product-is-empty : is-equiv (pr2 {A = A} {B = λ a → B})
is-equiv-pr2-product-is-empty =
is-equiv-is-invertible
inv-pr2-product-is-empty
is-section-inv-pr2-product-is-empty
is-retraction-inv-pr2-product-is-empty

right-zero-law-product-is-empty : (A × B) ≃ B
pr1 right-zero-law-product-is-empty = pr2
pr2 right-zero-law-product-is-empty = is-equiv-pr2-product-is-empty


### Right absorption law for dependent pair types and for cartesian products

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

map-right-absorption-Σ : Σ A (λ x → empty) → empty
map-right-absorption-Σ (pair x ())

is-equiv-map-right-absorption-Σ : is-equiv map-right-absorption-Σ
is-equiv-map-right-absorption-Σ = is-equiv-is-empty' map-right-absorption-Σ

right-absorption-Σ : Σ A (λ x → empty) ≃ empty
right-absorption-Σ =
pair map-right-absorption-Σ is-equiv-map-right-absorption-Σ


### Left absorption law for dependent pair types

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

map-left-absorption-Σ : Σ empty A → empty
map-left-absorption-Σ = pr1

is-equiv-map-left-absorption-Σ : is-equiv map-left-absorption-Σ
is-equiv-map-left-absorption-Σ =
is-equiv-is-empty' map-left-absorption-Σ

left-absorption-Σ : Σ empty A ≃ empty
pr1 left-absorption-Σ = map-left-absorption-Σ
pr2 left-absorption-Σ = is-equiv-map-left-absorption-Σ


### Right absorption law for cartesian product types

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

map-right-absorption-product : A × empty → empty
map-right-absorption-product = map-right-absorption-Σ A

is-equiv-map-right-absorption-product : is-equiv map-right-absorption-product
is-equiv-map-right-absorption-product = is-equiv-map-right-absorption-Σ A

right-absorption-product : (A × empty) ≃ empty
right-absorption-product = right-absorption-Σ A

is-empty-right-factor-is-empty-product :
{l1 l2 : Level} {A : UU l1} {B : UU l2} → is-empty (A × B) → A → is-empty B
is-empty-right-factor-is-empty-product f a b = f (pair a b)


### Left absorption law for cartesian products

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

map-left-absorption-product : empty × A → empty
map-left-absorption-product = map-left-absorption-Σ (λ x → A)

is-equiv-map-left-absorption-product : is-equiv map-left-absorption-product
is-equiv-map-left-absorption-product =
is-equiv-map-left-absorption-Σ (λ x → A)

left-absorption-product : (empty × A) ≃ empty
left-absorption-product = left-absorption-Σ (λ x → A)

is-empty-left-factor-is-empty-product :
{l1 l2 : Level} {A : UU l1} {B : UU l2} → is-empty (A × B) → B → is-empty A
is-empty-left-factor-is-empty-product f b a = f (pair a b)


### Left unit law for coproducts

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

map-left-unit-law-coproduct-is-empty : A + B → B
map-left-unit-law-coproduct-is-empty (inl a) = ex-falso (H a)
map-left-unit-law-coproduct-is-empty (inr b) = b

map-inv-left-unit-law-coproduct-is-empty : B → A + B
map-inv-left-unit-law-coproduct-is-empty = inr

is-section-map-inv-left-unit-law-coproduct-is-empty :
( map-left-unit-law-coproduct-is-empty ∘
map-inv-left-unit-law-coproduct-is-empty) ~ id
is-section-map-inv-left-unit-law-coproduct-is-empty = refl-htpy

is-retraction-map-inv-left-unit-law-coproduct-is-empty :
( map-inv-left-unit-law-coproduct-is-empty ∘
map-left-unit-law-coproduct-is-empty) ~ id
is-retraction-map-inv-left-unit-law-coproduct-is-empty (inl a) =
ex-falso (H a)
is-retraction-map-inv-left-unit-law-coproduct-is-empty (inr b) = refl

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

left-unit-law-coproduct-is-empty : (A + B) ≃ B
pr1 left-unit-law-coproduct-is-empty = map-left-unit-law-coproduct-is-empty
pr2 left-unit-law-coproduct-is-empty =
is-equiv-map-left-unit-law-coproduct-is-empty

is-equiv-inr-is-empty :
is-equiv inr
is-equiv-inr-is-empty =
is-equiv-is-invertible
( map-left-unit-law-coproduct-is-empty)
( is-retraction-map-inv-left-unit-law-coproduct-is-empty)
( is-section-map-inv-left-unit-law-coproduct-is-empty)

inv-left-unit-law-coproduct-is-empty : B ≃ (A + B)
pr1 inv-left-unit-law-coproduct-is-empty =
map-inv-left-unit-law-coproduct-is-empty
pr2 inv-left-unit-law-coproduct-is-empty = is-equiv-inr-is-empty

is-contr-map-left-unit-law-coproduct-is-empty :
is-contr-map map-left-unit-law-coproduct-is-empty
is-contr-map-left-unit-law-coproduct-is-empty =
is-contr-map-is-equiv is-equiv-map-left-unit-law-coproduct-is-empty

is-contr-map-inr-is-empty :
is-contr-map map-inv-left-unit-law-coproduct-is-empty
is-contr-map-inr-is-empty = is-contr-map-is-equiv is-equiv-inr-is-empty

is-right-coproduct-is-empty : (x : A + B) → Σ B (λ b → inr b ＝ x)
is-right-coproduct-is-empty x = center (is-contr-map-inr-is-empty x)

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

is-empty-left-summand-is-equiv : is-equiv (inr {A = A} {B = B}) → is-empty A
is-empty-left-summand-is-equiv H a =
neq-inr-inl (is-section-map-inv-is-equiv H (inl a))

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

map-left-unit-law-coproduct : empty + B → B
map-left-unit-law-coproduct = map-left-unit-law-coproduct-is-empty empty B id

map-inv-left-unit-law-coproduct : B → empty + B
map-inv-left-unit-law-coproduct = inr

is-section-map-inv-left-unit-law-coproduct :
( map-left-unit-law-coproduct ∘ map-inv-left-unit-law-coproduct) ~ id
is-section-map-inv-left-unit-law-coproduct =
is-section-map-inv-left-unit-law-coproduct-is-empty empty B id

is-retraction-map-inv-left-unit-law-coproduct :
( map-inv-left-unit-law-coproduct ∘ map-left-unit-law-coproduct) ~ id
is-retraction-map-inv-left-unit-law-coproduct =
is-retraction-map-inv-left-unit-law-coproduct-is-empty empty B id

is-equiv-map-left-unit-law-coproduct : is-equiv map-left-unit-law-coproduct
is-equiv-map-left-unit-law-coproduct =
is-equiv-map-left-unit-law-coproduct-is-empty empty B id

left-unit-law-coproduct : (empty + B) ≃ B
left-unit-law-coproduct = left-unit-law-coproduct-is-empty empty B id

inv-left-unit-law-coproduct : B ≃ (empty + B)
inv-left-unit-law-coproduct = inv-left-unit-law-coproduct-is-empty empty B id


### Right unit law for coproducts

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

map-right-unit-law-coproduct-is-empty : A + B → A
map-right-unit-law-coproduct-is-empty (inl a) = a
map-right-unit-law-coproduct-is-empty (inr b) = ex-falso (H b)

map-inv-right-unit-law-coproduct-is-empty : A → A + B
map-inv-right-unit-law-coproduct-is-empty = inl

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

is-retraction-map-inv-right-unit-law-coproduct-is-empty :
( map-inv-right-unit-law-coproduct-is-empty ∘
map-right-unit-law-coproduct-is-empty) ~ id
is-retraction-map-inv-right-unit-law-coproduct-is-empty (inl a) = refl
is-retraction-map-inv-right-unit-law-coproduct-is-empty (inr b) =
ex-falso (H b)

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

is-equiv-inl-is-empty : is-equiv (inl {l1} {l2} {A} {B})
is-equiv-inl-is-empty =
is-equiv-is-invertible
( map-right-unit-law-coproduct-is-empty)
( is-retraction-map-inv-right-unit-law-coproduct-is-empty)
( is-section-map-inv-right-unit-law-coproduct-is-empty)

right-unit-law-coproduct-is-empty : (A + B) ≃ A
pr1 right-unit-law-coproduct-is-empty = map-right-unit-law-coproduct-is-empty
pr2 right-unit-law-coproduct-is-empty =
is-equiv-map-right-unit-law-coproduct-is-empty

inv-right-unit-law-coproduct-is-empty : A ≃ (A + B)
pr1 inv-right-unit-law-coproduct-is-empty = inl
pr2 inv-right-unit-law-coproduct-is-empty = is-equiv-inl-is-empty

is-contr-map-right-unit-law-coproduct-is-empty :
is-contr-map map-right-unit-law-coproduct-is-empty
is-contr-map-right-unit-law-coproduct-is-empty =
is-contr-map-is-equiv is-equiv-map-right-unit-law-coproduct-is-empty

is-contr-map-inl-is-empty : is-contr-map inl
is-contr-map-inl-is-empty = is-contr-map-is-equiv is-equiv-inl-is-empty

is-left-coproduct-is-empty :
(x : A + B) → Σ A (λ a → inl a ＝ x)
is-left-coproduct-is-empty x = center (is-contr-map-inl-is-empty x)

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

is-empty-right-summand-is-equiv : is-equiv (inl {A = A} {B = B}) → is-empty B
is-empty-right-summand-is-equiv H b =
neq-inl-inr (is-section-map-inv-is-equiv H (inr b))

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

map-right-unit-law-coproduct : A + empty → A
map-right-unit-law-coproduct =
map-right-unit-law-coproduct-is-empty A empty id

map-inv-right-unit-law-coproduct : A → A + empty
map-inv-right-unit-law-coproduct = inl

is-section-map-inv-right-unit-law-coproduct :
( map-right-unit-law-coproduct ∘ map-inv-right-unit-law-coproduct) ~ id
is-section-map-inv-right-unit-law-coproduct =
is-section-map-inv-right-unit-law-coproduct-is-empty A empty id

is-retraction-map-inv-right-unit-law-coproduct :
( map-inv-right-unit-law-coproduct ∘ map-right-unit-law-coproduct) ~ id
is-retraction-map-inv-right-unit-law-coproduct =
is-retraction-map-inv-right-unit-law-coproduct-is-empty A empty id

is-equiv-map-right-unit-law-coproduct : is-equiv map-right-unit-law-coproduct
is-equiv-map-right-unit-law-coproduct =
is-equiv-map-right-unit-law-coproduct-is-empty A empty id

right-unit-law-coproduct : (A + empty) ≃ A
right-unit-law-coproduct = right-unit-law-coproduct-is-empty A empty id

inv-right-unit-law-coproduct : A ≃ (A + empty)
inv-right-unit-law-coproduct =
inv-right-unit-law-coproduct-is-empty A empty id