sigma.idr

infixr 5 :>
data Vect : Nat -> Type -> Type where
  Empty : Vect Z a
  (:>)  : a -> Vect n a -> Vect (S n) a

data Sigma : (a : Type) -> (P : a -> Type) -> Type where
  MkSigma : {P : a -> Type} -> (x : a) -> P x -> Sigma a P

vec : Sigma Nat (\n => Vect n Int)
vec = MkSigma 2 (3:>4:>Empty)

vec' : Sigma Nat (\n => Vect n Int)
vec' = MkSigma _ (3:>4:>Empty)

len : Vect n a -> Sigma Nat (\m => n = m)
len {n} _ = MkSigma (S n) Refl