@@ -0,0 +1,17 @@
1+data Tag : String -> List String -> Type where
2+ TZ : Tag l (l :: e)
3+ TS : Tag l e -> Tag l (l' :: e)
4+
5+SPi : (e : List String)
6+ -> ((l : String) -> Tag l e -> Type)
7+ -> Type
8+SPi [] _ = ()
9+SPi (l :: e) prop = (prop l TZ, SPi e $ \l' => \t => prop l' $ TS t)
10+
11+switch : (e : List String)
12+ -> (prop : (l : String) -> (t : Tag l e) -> Type)
13+ -> SPi e prop
14+ -> (l' : String) -> (t' : Tag l' e) -> prop l' t'
15+switch (l' :: e) prop ((propz, props)) l' TZ = propz
16+switch (l :: e) prop ((propz, props)) l' (TS t') =
17+ switch e (\l => \t => prop l (TS t)) props l' t'