Sigma+Nat suffice for ADTs

AndOr.idr

module AndOr

%default total
%access private

TData : Type -> Type -> Nat -> Type
TData a _ Z = a
TData a b (S Z) = (a, b)
TData _ b (S (S Z)) = b
TData _ _ _ = Void

export
AndOr : Type -> Type -> Type
AndOr a b = DPair Nat (TData a b)

export
Left : a -> AndOr a b
Left x = (Z ** x)

export
Middle : a -> b -> AndOr a b
Middle x y = (S Z ** (x, y))

export
Right : b -> AndOr a b
Right x = (S (S Z) ** x)

only_three_constructors : (n : Nat) -> TData a b (S (S (S n))) = Void
only_three_constructors Z = Refl
only_three_constructors (S _) = Refl

export
elim : (a -> z) -> ((a, b) -> z) -> (b -> z) -> AndOr a b -> z
elim f _ _ (Z ** x) = f x
elim _ g _ (S Z ** x) = g x
elim _ _ h (S (S Z) ** x) = h x
elim _ _ _ (S (S (S _)) ** _) impossible

export
map : (r -> s) -> AndOr l r -> AndOr l s
map f = elim (Left .id) (\(a, b) => Middle a (f b)) (Right . f)

VecList.idr

module VecList

%default total
%access private

fold : (a -> a) -> a -> Nat -> a
fold _ x Z = x
fold f x (S k) = fold f (f x) k

export
Vec : Nat -> Type -> Type
Vec n t = fold (Pair t) () n

export
List : Type -> Type
List t = (n : Nat ** Vec n t)

Nil : Vec Z a
Nil = ()

vectors_built_of_cons_cells : (a : Type) -> (n : Nat) -> Vec (S n) a = (a, Vec n a)
vectors_built_of_cons_cells _ Z = Refl
vectors_built_of_cons_cells a (S k) =
  let x = vectors_built_of_cons_cells a k in ?halp

--Cons : a -> Vec n a -> Vec (S n) a
--Cons x y = (x, y)

--map : (a -> b) -> Vec n a -> Vec n b
--map {n = Z} _ _ = ()
--map {n = (S _)} f (x, xs) = Cons (f x) (map f xs)