EITHER

-type is a representation disjunction.

Constructors

Eliminators

Induction Principle