# Coproduct types

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

Created on 2022-01-27.

module foundation.coproduct-types where

open import foundation-core.coproduct-types public

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.negated-equality
open import foundation.noncontractible-types
open import foundation.subuniverses
open import foundation.unit-type
open import foundation.universe-levels

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
open import foundation-core.injective-maps
open import foundation-core.negation
open import foundation-core.propositions


### The predicates of being in the left and in the right summand

module _
{l1 l2 : Level} {X : UU l1} {Y : UU l2}
where

is-left-Prop : X + Y → Prop lzero
is-left-Prop (inl x) = unit-Prop
is-left-Prop (inr x) = empty-Prop

is-left : X + Y → UU lzero
is-left x = type-Prop (is-left-Prop x)

is-prop-is-left : (x : X + Y) → is-prop (is-left x)
is-prop-is-left x = is-prop-type-Prop (is-left-Prop x)

is-right-Prop : X + Y → Prop lzero
is-right-Prop (inl x) = empty-Prop
is-right-Prop (inr x) = unit-Prop

is-right : X + Y → UU lzero
is-right x = type-Prop (is-right-Prop x)

is-prop-is-right : (x : X + Y) → is-prop (is-right x)
is-prop-is-right x = is-prop-type-Prop (is-right-Prop x)

is-left-or-is-right : (x : X + Y) → is-left x + is-right x
is-left-or-is-right (inl x) = inl star
is-left-or-is-right (inr x) = inr star


### The predicate that a subuniverse is closed under coproducts

We formulate a variant with three subuniverses and the more traditional variant using a single subuniverse

is-closed-under-coproducts-subuniverses :
{l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2) (Q : subuniverse l3 l4) →
subuniverse (l1 ⊔ l3) l5 → UU (lsuc l1 ⊔ l2 ⊔ lsuc l3 ⊔ l4 ⊔ l5)
is-closed-under-coproducts-subuniverses {l1} {l2} {l3} P Q R =
{X : UU l1} {Y : UU l3} →
is-in-subuniverse P X → is-in-subuniverse Q Y → is-in-subuniverse R (X + Y)

is-closed-under-coproducts-subuniverse :
{l1 l2 : Level} (P : subuniverse l1 l2) → UU (lsuc l1 ⊔ l2)
is-closed-under-coproducts-subuniverse P =
is-closed-under-coproducts-subuniverses P P P


## Properties

### The left and right inclusions are injective

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

is-injective-inl : is-injective {B = A + B} inl
is-injective-inl refl = refl

is-injective-inr : is-injective {B = A + B} inr
is-injective-inr refl = refl

neq-inl-inr : {x : A} {y : B} → inl x ≠ inr y
neq-inl-inr ()

neq-inr-inl : {x : B} {y : A} → inr x ≠ inl y
neq-inr-inl ()


### The type of left elements is equivalent to the left summand

module _
{l1 l2 : Level} {X : UU l1} {Y : UU l2}
where

map-equiv-left-summand : Σ (X + Y) is-left → X
map-equiv-left-summand (inl x , star) = x
map-equiv-left-summand (inr x , ())

map-inv-equiv-left-summand : X → Σ (X + Y) is-left
pr1 (map-inv-equiv-left-summand x) = inl x
pr2 (map-inv-equiv-left-summand x) = star

is-section-map-inv-equiv-left-summand :
(map-equiv-left-summand ∘ map-inv-equiv-left-summand) ~ id
is-section-map-inv-equiv-left-summand x = refl

is-retraction-map-inv-equiv-left-summand :
(map-inv-equiv-left-summand ∘ map-equiv-left-summand) ~ id
is-retraction-map-inv-equiv-left-summand (inl x , star) = refl
is-retraction-map-inv-equiv-left-summand (inr x , ())

equiv-left-summand : (Σ (X + Y) is-left) ≃ X
pr1 equiv-left-summand = map-equiv-left-summand
pr2 equiv-left-summand =
is-equiv-is-invertible
map-inv-equiv-left-summand
is-section-map-inv-equiv-left-summand
is-retraction-map-inv-equiv-left-summand


### The type of right elements is equivalent to the right summand

module _
{l1 l2 : Level} {X : UU l1} {Y : UU l2}
where

map-equiv-right-summand : Σ (X + Y) is-right → Y
map-equiv-right-summand (inl x , ())
map-equiv-right-summand (inr x , star) = x

map-inv-equiv-right-summand : Y → Σ (X + Y) is-right
pr1 (map-inv-equiv-right-summand y) = inr y
pr2 (map-inv-equiv-right-summand y) = star

is-section-map-inv-equiv-right-summand :
map-equiv-right-summand ∘ map-inv-equiv-right-summand ~ id
is-section-map-inv-equiv-right-summand y = refl

is-retraction-map-inv-equiv-right-summand :
map-inv-equiv-right-summand ∘ map-equiv-right-summand ~ id
is-retraction-map-inv-equiv-right-summand (inl x , ())
is-retraction-map-inv-equiv-right-summand (inr x , star) = refl

equiv-right-summand : Σ (X + Y) is-right ≃ Y
pr1 equiv-right-summand = map-equiv-right-summand
pr2 equiv-right-summand =
is-equiv-is-invertible
map-inv-equiv-right-summand
is-section-map-inv-equiv-right-summand
is-retraction-map-inv-equiv-right-summand


### Coproducts of contractible types are not contractible

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

abstract
is-not-contractible-coproduct-is-contr :
is-contr A → is-contr B → is-not-contractible (A + B)
is-not-contractible-coproduct-is-contr HA HB HAB =
neq-inl-inr {x = center HA} {y = center HB} (eq-is-contr HAB)


### Coproducts of mutually exclusive propositions are propositions

module _
{l1 l2 : Level} {P : UU l1} {Q : UU l2}
where

abstract
all-elements-equal-coproduct :
(P → ¬ Q) → all-elements-equal P → all-elements-equal Q →
all-elements-equal (P + Q)
all-elements-equal-coproduct f is-prop-P is-prop-Q (inl p) (inl p') =
ap inl (is-prop-P p p')
all-elements-equal-coproduct f is-prop-P is-prop-Q (inl p) (inr q') =
ex-falso (f p q')
all-elements-equal-coproduct f is-prop-P is-prop-Q (inr q) (inl p') =
ex-falso (f p' q)
all-elements-equal-coproduct f is-prop-P is-prop-Q (inr q) (inr q') =
ap inr (is-prop-Q q q')

abstract
is-prop-coproduct : (P → ¬ Q) → is-prop P → is-prop Q → is-prop (P + Q)
is-prop-coproduct f is-prop-P is-prop-Q =
is-prop-all-elements-equal
( all-elements-equal-coproduct f
( eq-is-prop' is-prop-P)
( eq-is-prop' is-prop-Q))

coproduct-Prop :
{l1 l2 : Level} (P : Prop l1) (Q : Prop l2) →
(type-Prop P → ¬ (type-Prop Q)) → Prop (l1 ⊔ l2)
pr1 (coproduct-Prop P Q H) =
type-Prop P + type-Prop Q
pr2 (coproduct-Prop P Q H) =
is-prop-coproduct H (is-prop-type-Prop P) (is-prop-type-Prop Q)