Table of Contents

1 Prelude

2 Coproduct Types

The coproduct of two types is defined inductively by elements from each type.

data _+_ {i j : Level} (A : Type i) (B : Type j) : Type (i  j) where
  inl : A  A + B
  inr : B  A + B

3 Induction

The induction principle can be defined as follows:

coproduct-ind :  {i j k} {A : Type i} {B : Type j} {C : Type k}
              (A  C)  (B  C)
              A + B  C
coproduct-ind x x₁ (inl x₂) = x x₂
coproduct-ind x x₁ (inr x₂) = x₁ x₂

4 Coproduct commutes

Author: James Leslie

Created: 2021-03-27 Sat 10:47