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