Coproduct types

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

Created on 2023-01-20.
Last modified on 2024-04-11.

module foundation-core.coproduct-types where
open import foundation.universe-levels


The coproduct of two types A and B can be thought of as the disjoint union of A and B.


Coproduct types

infixr 10 _+_

data _+_ {l1 l2 : Level} (A : UU l1) (B : UU l2) : UU (l1  l2)
  inl : A  A + B
  inr : B  A + B

The induction principle for coproduct types

ind-coproduct :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (C : A + B  UU l3) 
  ((x : A)  C (inl x))  ((y : B)  C (inr y)) 
  (t : A + B)  C t
ind-coproduct C f g (inl x) = f x
ind-coproduct C f g (inr x) = g x

The recursion principle for coproduct types

rec-coproduct :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} 
  (A  C)  (B  C)  (A + B)  C
rec-coproduct {C = C} = ind-coproduct  _  C)

Recent changes