Pi-type over a list in dependent type theory In a formalization I need to create an inductive type which has a term for each element in a list, something like this (I'll use Agda in the following, but everything here is standard dependent type theory):
data DataType : Type where
  inj : (xs : List A) → (x : {! xs !}) → DataType

Of course, we cannot have a Pi type over x : xs in the middle since xs is a term and not a type, so we cannot quantify over it.
We can use singletons to get an n-tuple from a list as follows:
Singleton : (x : A) → Type
Singleton x = Σ[ y ∈ A ] (y ≡ x)

list→type : List A → Type
list→type [] = ⊥
list→type (x ∷ []) = Singleton x
list→type (x ∷ y ∷ xs) = Singleton x × list→type (y ∷ xs)

That way a list 1 ∷ 2 ∷ 3 ∷ [] is turned into the tuple (s1, s2, s3), from which can recover the numbers in the list. However, this tuple is still just one term, so we will only have a single inj (s1, s2, s3) in our data type above when using list→type xs in the Pi type above.
How can we get a different inhabitant in DataType for each element of the list? Is there a standard way to deal with that? Or do I fundamentally misunderstand something? It's of course a bit awkward to mix a data structure understanding of &quot;collection&quot; with the basic doctrine of regarding types as collections (with explicit term constructors), but it still should be possible to reconcile both understandings I hope.
You asked several questions.
You asked about a type indexed by a list, so you can do this.
data DataType (A : Type) (F : A -&gt; Type) : List A -&gt; Type where
  empty : DataType A F []
  _bla_ : forall {xs} {x} -&gt; DataType A F xs -&gt; F x -&gt; DataType A F (x ∷ xs)

Where F is a type family that is indexed by the elements of the list.
Apart from that, you mentioned tuples. Probably you want a sized vector (Data.Vec in stdlib) for tuples. For instance, Vec Nat 3 is such a type that 1 ∷ 2 ∷ [] and 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] are both invalid instances, only 1 ∷ 2 ∷ 3 ∷ [] is.