module Haskell.Law.Either where open import Haskell.Prim open import Haskell.Prim.Either open import Haskell.Law.Def Left-injective : Injective (Left {a}{b}) Left-injective refl = refl Right-injective : Injective (Right {a}{b}) Right-injective refl = refl