source: Deliverables/D4.1/Matita/Either.ma @ 327

include "Bool.ma".
include "Maybe.ma".

include "Universes.ma".

ninductive Either (A: Type[0]) (B: Type[0]): Type[0] ≝
  Left: A → Either A B
| Right: B → Either A B.

notation "hvbox(a break ⊎ b)"
 left associative with precedence 50
for @{ 'disjoint_union $a $b }.
interpretation "Either" 'disjoint_union A B = (Either A B).

ndefinition is_left ≝
  λA, B: Type[0].
  λe: Either A B.
    match e with
      [ Left l ⇒ true
      | Right r ⇒ false
      ].
      
ndefinition is_right ≝
  λA, B: Type[0].
  λe: Either A B.
    match e with
      [ Left l ⇒ false
      | Right r ⇒ true
      ].

ndefinition either ≝
  λA, B, C: Type[0].
  λf: A → C.
  λg: B → C.
  λe: Either A B.
    match e with
      [ Left l ⇒ f l
      | Right r ⇒ g r
      ].
      
ndefinition map_left ≝
  λA, B, C: Type[0].
  λf: A → C.
  λe: Either A B.
    match e with
      [ Left l ⇒ Left C B (f l)
      | Right r ⇒ Right C B r
      ].
      
ndefinition map_right ≝
  λA, B, C: Type[0].
  λf: B → C.
  λe: Either A B.
    match e with
      [ Left l ⇒ Left A C l
      | Right r ⇒ Right A C (f r)
      ].
      
ndefinition map_both ≝
  λA, B, C, D: Type[0].
  λf: A → C.
  λg: B → D.
  λe: Either A B.
    match e with
      [ Left l ⇒ Left C D (f l)
      | Right r ⇒ Right C D (g r)
      ].