Module Either

Meta-data

Contents

data Either (a : Type) (b : Type) where
    Left a
  ; Right b

pushEither : forall {a : Type, b : Type, c : Nat} 
           . {c ≤ 1} =>
    ((Either a b) [c]) -> Either (a [c]) (b [c])

pullEither : forall {a : Type, b : Type, c : Nat} 
           . (Either (a [c]) (b [c])) -> (Either a b) [c]
Distrbute a graded modality outside Either