LiamGoodacre

-- We define uncurried versions of Pair and Either to help with type-checking
data Tuple : (Type, Type) -> Type where 
  MkTuple : a -> b -> Tuple (a, b)

data Sum : (Type, Type) -> Type where 
  Left : a -> Sum (a, b)
  Right : b -> Sum (a, b)

-- These are bifunctor versions of projections/injections
data Fst : (Type, Type) -> Type where