# Type arithmetic for coproduct types

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

Created on 2022-01-27.

module foundation.type-arithmetic-coproduct-types where

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

open import foundation-core.cartesian-product-types
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 laws for the manipulation of coproduct types with respect to themselves, cartesian products, and dependent pair types.

## Laws

### Commutativity of coproducts

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

map-commutative-coproduct : A + B → B + A
map-commutative-coproduct (inl a) = inr a
map-commutative-coproduct (inr b) = inl b

map-inv-commutative-coproduct : B + A → A + B
map-inv-commutative-coproduct (inl b) = inr b
map-inv-commutative-coproduct (inr a) = inl a

is-section-map-inv-commutative-coproduct :
( map-commutative-coproduct ∘ map-inv-commutative-coproduct) ~ id
is-section-map-inv-commutative-coproduct (inl b) = refl
is-section-map-inv-commutative-coproduct (inr a) = refl

is-retraction-map-inv-commutative-coproduct :
( map-inv-commutative-coproduct ∘ map-commutative-coproduct) ~ id
is-retraction-map-inv-commutative-coproduct (inl a) = refl
is-retraction-map-inv-commutative-coproduct (inr b) = refl

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

commutative-coproduct : (A + B) ≃ (B + A)
pr1 commutative-coproduct = map-commutative-coproduct
pr2 commutative-coproduct = is-equiv-map-commutative-coproduct


### Associativity of coproducts

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

map-associative-coproduct : (A + B) + C → A + (B + C)
map-associative-coproduct (inl (inl x)) = inl x
map-associative-coproduct (inl (inr x)) = inr (inl x)
map-associative-coproduct (inr x) = inr (inr x)

map-inv-associative-coproduct : A + (B + C) → (A + B) + C
map-inv-associative-coproduct (inl x) = inl (inl x)
map-inv-associative-coproduct (inr (inl x)) = inl (inr x)
map-inv-associative-coproduct (inr (inr x)) = inr x

is-section-map-inv-associative-coproduct :
(map-associative-coproduct ∘ map-inv-associative-coproduct) ~ id
is-section-map-inv-associative-coproduct (inl x) = refl
is-section-map-inv-associative-coproduct (inr (inl x)) = refl
is-section-map-inv-associative-coproduct (inr (inr x)) = refl

is-retraction-map-inv-associative-coproduct :
(map-inv-associative-coproduct ∘ map-associative-coproduct) ~ id
is-retraction-map-inv-associative-coproduct (inl (inl x)) = refl
is-retraction-map-inv-associative-coproduct (inl (inr x)) = refl
is-retraction-map-inv-associative-coproduct (inr x) = refl

is-equiv-map-associative-coproduct : is-equiv map-associative-coproduct
is-equiv-map-associative-coproduct =
is-equiv-is-invertible
map-inv-associative-coproduct
is-section-map-inv-associative-coproduct
is-retraction-map-inv-associative-coproduct

is-equiv-map-inv-associative-coproduct :
is-equiv map-inv-associative-coproduct
is-equiv-map-inv-associative-coproduct =
is-equiv-is-invertible
map-associative-coproduct
is-retraction-map-inv-associative-coproduct
is-section-map-inv-associative-coproduct

associative-coproduct : ((A + B) + C) ≃ (A + (B + C))
pr1 associative-coproduct = map-associative-coproduct
pr2 associative-coproduct = is-equiv-map-associative-coproduct

inv-associative-coproduct : (A + (B + C)) ≃ ((A + B) + C)
pr1 inv-associative-coproduct = map-inv-associative-coproduct
pr2 inv-associative-coproduct = is-equiv-map-inv-associative-coproduct


### Right distributivity of Σ over coproducts

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

map-right-distributive-Σ-coproduct :
Σ (A + B) C → (Σ A (λ x → C (inl x))) + (Σ B (λ y → C (inr y)))
map-right-distributive-Σ-coproduct (inl x , z) = inl (x , z)
map-right-distributive-Σ-coproduct (inr y , z) = inr (y , z)

map-inv-right-distributive-Σ-coproduct :
(Σ A (λ x → C (inl x))) + (Σ B (λ y → C (inr y))) → Σ (A + B) C
pr1 (map-inv-right-distributive-Σ-coproduct (inl (x , z))) = inl x
pr2 (map-inv-right-distributive-Σ-coproduct (inl (x , z))) = z
pr1 (map-inv-right-distributive-Σ-coproduct (inr (y , z))) = inr y
pr2 (map-inv-right-distributive-Σ-coproduct (inr (y , z))) = z

is-section-map-inv-right-distributive-Σ-coproduct :
( map-right-distributive-Σ-coproduct ∘
map-inv-right-distributive-Σ-coproduct) ~
( id)
is-section-map-inv-right-distributive-Σ-coproduct (inl (x , z)) = refl
is-section-map-inv-right-distributive-Σ-coproduct (inr (y , z)) = refl

is-retraction-map-inv-right-distributive-Σ-coproduct :
( map-inv-right-distributive-Σ-coproduct ∘
map-right-distributive-Σ-coproduct) ~
( id)
is-retraction-map-inv-right-distributive-Σ-coproduct (inl x , z) = refl
is-retraction-map-inv-right-distributive-Σ-coproduct (inr y , z) = refl

abstract
is-equiv-map-right-distributive-Σ-coproduct :
is-equiv map-right-distributive-Σ-coproduct
is-equiv-map-right-distributive-Σ-coproduct =
is-equiv-is-invertible
map-inv-right-distributive-Σ-coproduct
is-section-map-inv-right-distributive-Σ-coproduct
is-retraction-map-inv-right-distributive-Σ-coproduct

right-distributive-Σ-coproduct :
Σ (A + B) C ≃ ((Σ A (λ x → C (inl x))) + (Σ B (λ y → C (inr y))))
pr1 right-distributive-Σ-coproduct = map-right-distributive-Σ-coproduct
pr2 right-distributive-Σ-coproduct =
is-equiv-map-right-distributive-Σ-coproduct


### Left distributivity of Σ over coproducts

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

map-left-distributive-Σ-coproduct :
Σ A (λ x → B x + C x) → (Σ A B) + (Σ A C)
map-left-distributive-Σ-coproduct (x , inl y) = inl (x , y)
map-left-distributive-Σ-coproduct (x , inr z) = inr (x , z)

map-inv-left-distributive-Σ-coproduct :
(Σ A B) + (Σ A C) → Σ A (λ x → B x + C x)
pr1 (map-inv-left-distributive-Σ-coproduct (inl (x , y))) = x
pr2 (map-inv-left-distributive-Σ-coproduct (inl (x , y))) = inl y
pr1 (map-inv-left-distributive-Σ-coproduct (inr (x , z))) = x
pr2 (map-inv-left-distributive-Σ-coproduct (inr (x , z))) = inr z

is-section-map-inv-left-distributive-Σ-coproduct :
( map-left-distributive-Σ-coproduct ∘
map-inv-left-distributive-Σ-coproduct) ~
( id)
is-section-map-inv-left-distributive-Σ-coproduct (inl (x , y)) = refl
is-section-map-inv-left-distributive-Σ-coproduct (inr (x , z)) = refl

is-retraction-map-inv-left-distributive-Σ-coproduct :
( map-inv-left-distributive-Σ-coproduct ∘
map-left-distributive-Σ-coproduct) ~
( id)
is-retraction-map-inv-left-distributive-Σ-coproduct (x , inl y) = refl
is-retraction-map-inv-left-distributive-Σ-coproduct (x , inr z) = refl

is-equiv-map-left-distributive-Σ-coproduct :
is-equiv map-left-distributive-Σ-coproduct
is-equiv-map-left-distributive-Σ-coproduct =
is-equiv-is-invertible
map-inv-left-distributive-Σ-coproduct
is-section-map-inv-left-distributive-Σ-coproduct
is-retraction-map-inv-left-distributive-Σ-coproduct

left-distributive-Σ-coproduct :
Σ A (λ x → B x + C x) ≃ ((Σ A B) + (Σ A C))
pr1 left-distributive-Σ-coproduct = map-left-distributive-Σ-coproduct
pr2 left-distributive-Σ-coproduct = is-equiv-map-left-distributive-Σ-coproduct


### Right distributivity of products over coproducts

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

map-right-distributive-product-coproduct : (A + B) × C → (A × C) + (B × C)
map-right-distributive-product-coproduct =
map-right-distributive-Σ-coproduct A B (λ _ → C)

map-inv-right-distributive-product-coproduct :
(A × C) + (B × C) → (A + B) × C
map-inv-right-distributive-product-coproduct =
map-inv-right-distributive-Σ-coproduct A B (λ _ → C)

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

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

abstract
is-equiv-map-right-distributive-product-coproduct :
is-equiv map-right-distributive-product-coproduct
is-equiv-map-right-distributive-product-coproduct =
is-equiv-map-right-distributive-Σ-coproduct A B (λ _ → C)

right-distributive-product-coproduct : ((A + B) × C) ≃ ((A × C) + (B × C))
right-distributive-product-coproduct =
right-distributive-Σ-coproduct A B (λ _ → C)


### Left distributivity of products over coproducts

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

map-left-distributive-product-coproduct : A × (B + C) → (A × B) + (A × C)
map-left-distributive-product-coproduct =
map-left-distributive-Σ-coproduct A (λ _ → B) (λ _ → C)

map-inv-left-distributive-product-coproduct :
(A × B) + (A × C) → A × (B + C)
map-inv-left-distributive-product-coproduct =
map-inv-left-distributive-Σ-coproduct A (λ _ → B) (λ _ → C)

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

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

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

left-distributive-product-coproduct : (A × (B + C)) ≃ ((A × B) + (A × C))
left-distributive-product-coproduct =
left-distributive-Σ-coproduct A (λ _ → B) (λ _ → C)


### If a coproduct is contractible then one summand is contractible and the other is empty

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

is-contr-left-summand :
is-contr (A + B) → A → is-contr A
pr1 (is-contr-left-summand H a) = a
pr2 (is-contr-left-summand H a) x =
is-injective-inl (eq-is-contr H {inl a} {inl x})

is-contr-left-summand-is-empty :
is-contr (A + B) → is-empty B → is-contr A
pr1 (is-contr-left-summand-is-empty (inl a , H) K) = a
pr2 (is-contr-left-summand-is-empty (inl a , H) K) x =
is-injective-inl (H (inl x))
is-contr-left-summand-is-empty (inr b , H) K = ex-falso (K b)

is-contr-right-summand :
is-contr (A + B) → B → is-contr B
pr1 (is-contr-right-summand H b) = b
pr2 (is-contr-right-summand H b) x =
is-injective-inr (eq-is-contr H {inr b} {inr x})

is-contr-right-summand-is-empty :
is-contr (A + B) → is-empty A → is-contr B
is-contr-right-summand-is-empty (inl a , H) K = ex-falso (K a)
pr1 (is-contr-right-summand-is-empty (inr b , H) K) = b
pr2 (is-contr-right-summand-is-empty (inr b , H) K) x =
is-injective-inr (H (inr x))

is-empty-left-summand-is-contr-coproduct :
is-contr (A + B) → B → is-empty A
is-empty-left-summand-is-contr-coproduct H b a =
ex-falso (is-empty-eq-coproduct-inl-inr a b (eq-is-contr H))

is-empty-right-summand-is-contr-coproduct :
is-contr (A + B) → A → is-empty B
is-empty-right-summand-is-contr-coproduct H a b =
ex-falso (is-empty-eq-coproduct-inl-inr a b (eq-is-contr H))