DISJOINT UNION

The disjoint union (sum type) is the type of values that are either from (tagged left) or from (tagged right). It is the coproduct in the category of types.

Formation

def + (A B: U) : U := Σ (x : 𝟐), ind₂ (λ (_ : 𝟐), U) A B x

Constructors

def inl (A B : U) (a : A) : + A B := (0₂, a)
def inr (A B : U) (b : B) : + A B := (>1₂, b)

Eliminators

The induction principle -ind allows case analysis on a value of the sum type.

def +-ind (A B : U) (C : + A B → U)
    (f : Π (x : A), C (inl A B x))
    (g : Π (y : B), C (inr A B y)) (w : + A B)
  : C w
 := ind₂ (λ (x : 𝟐), Π (u : ind₂ (λ (_ : 𝟐), U) A B x), C (x, u)) 
         f g w.1 w.2

Non-dependent recursion:

def +-rec (A B C : U) (f : A → C) (g : B → C)
  : (+ A B) → C
 := +-ind A B (λ (_ : + A B), C) f g

Computation Rules

The -rules for the disjoint union state how the eliminator computes on the constructors.

def +-β₁ (A B : U) (C : + A B → U) (a: A)
    (f : Π (x : A), C (inl A B x)) (g : Π (y : B), C (inr A B y))
  : PathP (<_>C (inl A B a)) (f a) (+-ind A B C f g (inl A B a))
 := <_> f a

def +-β₂ (A B : U) (C : + A B → U) (b: B)
    (f : Π (x : A), C (inl A B x)) (g : Π (y : B), C (inr A B y))
  : PathP (<_>C (inr A B b)) (g b) (+-ind A B C f g (inr A B b))
 := <_> g b

Uniqueness

def +-η (A B : U) (c : + A B)
  : + (Σ (x : A), PathP (<_> + A B) c (inl A B x))
      (Σ (y : B), PathP (<_> + A B) c (inr A B y))
 := +-ind A B (λ (c : + A B),
    + (Σ (x : A), PathP (<_> + A B) c (inl A B x))
      (Σ (y : B), PathP (<_> + A B) c (inr A B y)))
      (λ (x : A), (0₂, (x, <_> (0₂, x))))
      (λ (y : B), (>1₂, (y, <_> (>1₂, y)))) c

Finite Coproducts

Using , we can define small finite sum types such as , , , etc., with their corresponding eliminators.

def 𝟑 : U := + 𝟏 𝟐
def 0₃ : 𝟑 := inl 𝟏 𝟐 ★
def 1₃ : 𝟑 := inr 𝟏 𝟐 0₂
def 2₃ : 𝟑 := inr 𝟏 𝟐 1₂

def ind₃ (C : 𝟑 → U) (c₀ : C 0₃) (c₁ : C 1₃) (c₂ : C 2₃) 
  : Π (x : 𝟑), C x
 := +-ind 𝟏 𝟐 C (ind₁ (λ (_ : 𝟏), C 0₃) c₀) 
                (ind₂ (λ (_ : 𝟐), C (>1₂, _)) c₁ c₂)

Similar definitions exist for $𝟒$, $𝟓$, $𝟔$, $𝟕$ (see source module for full list).

Theorems

The disjoint union satisfies standard properties expected from a coproduct in type theory.