和型

module sum-type where

定義

infix  _+_
data _+_ (A B : Set) : Set where
  inl : A → A + B
  inr : B → A + B