Coproduct types

module foundation.coproduct-types where
Imports
open import foundation-core.coproduct-types public

open import foundation.noncontractible-types
open import foundation.subuniverses
open import foundation.unit-type

open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.functions
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
open import foundation-core.universe-levels

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 (pair (inl x) star) = x
  map-equiv-left-summand (pair (inr x) ())

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

  issec-map-inv-equiv-left-summand :
    (map-equiv-left-summand  map-inv-equiv-left-summand) ~ id
  issec-map-inv-equiv-left-summand x = refl

  isretr-map-inv-equiv-left-summand :
    (map-inv-equiv-left-summand  map-equiv-left-summand) ~ id
  isretr-map-inv-equiv-left-summand (pair (inl x) star) = refl
  isretr-map-inv-equiv-left-summand (pair (inr x) ())

  equiv-left-summand : (Σ (X + Y) is-left)  X
  pr1 equiv-left-summand = map-equiv-left-summand
  pr2 equiv-left-summand =
    is-equiv-has-inverse
      map-inv-equiv-left-summand
      issec-map-inv-equiv-left-summand
      isretr-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 (pair (inl x) ())
  map-equiv-right-summand (pair (inr x) star) = x

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

  issec-map-inv-equiv-right-summand :
    (map-equiv-right-summand  map-inv-equiv-right-summand) ~ id
  issec-map-inv-equiv-right-summand y = refl

  isretr-map-inv-equiv-right-summand :
    (map-inv-equiv-right-summand  map-equiv-right-summand) ~ id
  isretr-map-inv-equiv-right-summand (pair (inl x) ())
  isretr-map-inv-equiv-right-summand (pair (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-has-inverse
      map-inv-equiv-right-summand
      issec-map-inv-equiv-right-summand
      isretr-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-coprod-is-contr :
      is-contr A  is-contr B  is-not-contractible (A + B)
    is-not-contractible-coprod-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-coprod :
      (P  ¬ Q)  all-elements-equal P  all-elements-equal Q 
      all-elements-equal (P + Q)
    all-elements-equal-coprod f is-prop-P is-prop-Q (inl p) (inl p') =
      ap inl (is-prop-P p p')
    all-elements-equal-coprod f is-prop-P is-prop-Q (inl p) (inr q') =
      ex-falso (f p q')
    all-elements-equal-coprod f is-prop-P is-prop-Q (inr q) (inl p') =
      ex-falso (f p' q)
    all-elements-equal-coprod f is-prop-P is-prop-Q (inr q) (inr q') =
      ap inr (is-prop-Q q q')

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

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