Vect as W type

vect_as_vv.agda

{-# OPTIONS --type-in-type #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool

data Prod (L R : Set) : Set where
  pair : L -> R -> Prod L R

data Unit : Set where
  pt : Unit

data Sigma (A : Set)(f : A -> Set) : Set where
  sigma : (a : A) -> f a -> Sigma A f
  
data Void : Set where
  
W : (T : Set) -> (T -> Set) -> Set
W T f = Sigma T f

Vect : Nat -> Set -> Set
Vect n T = W Bool λ i -> f i n T where
  f : Bool -> Nat -> Set -> Set
  f false zero T = Unit
  f false (suc n) T = Void
  f true zero T = Void
  f true (suc n) T = Prod T (Vect n T)

test10 : Vect 3 Nat
test10 = sigma true (pair 1 (sigma true (pair 2 (sigma true (pair 3 (sigma false pt))))))


test11 : Vect 0 Nat
test11 = sigma true {!!} -- no introduction forms found!