Either_Polytype (L:*) (R:*) : *p
 = (Data:*) -> (L -> Data) -> (R -> Data) -> Data
Either (L:*) (R:*) : *m
 = Monotype (Either_Polytype L R)
Left (L:*) (R:*) (l:L) : Either L R
 = monotype (Either_Polytype L R)
    (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Left l)
Right (L:*) (R:*) (r:R) : Either L R
 = monotype (Either_Polytype L R)
    (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Right r)

left (L:*) (R:*) (l:L)
 : Either L R
 = monotype (Either_Polytype L R)
   (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Left l)
right (L:*) (R:*) (r:R)
 : Either L R
 = monotype (Either_Polytype L R)
   (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Right r)
either
 (L:*) (R:*) (Data:*)
 (l:L -> Data)
 (r:R -> Data)
 (e:Either L R)
 : Data
 = polytype (Either_Polytype L R) e Data l r

:load Monad.cloe
Monad_return_Either (L:*) (X:*)
 : Monad_Return (Either L) X
 = Right L X
Monad_bind_Either (L:*) (X:*) (Y:*)
 : Monad_Bind (Either L) X Y
 = λ(mx:Either L X) (my:X -> Either L Y) ->
     either L X (Either L Y) (Left L Y) my mx
Monad_Either (L:*)
 : Monad (Either L)
 = monad (Either L)
 (Monad_return_Either L)
 (Monad_bind_Either L)