# Family of types in type theory

Can anyone simplify the meaning of families of types index by a type. It looks i get it but quite not understood it. What do you mean by a "family" ?

I understand index by a value (n length sequence) then what you mean by index by a type. Any example how you index by a type ? Thanks.

Consider the example of the dependent type of number sequences of length $n$. It might be defined like this in Coq:

  Inductive Sequence : nat -> Type :=
| nil : Sequence O
| cons : forall (n : nat), nat -> Sequence n -> Sequence (S n).


For every n : nat we have a type Sequence n. We say that Sequence is indexed by nat or that Sequence depends on nat. We could also say that Sequence n depends on the index n.

In any case, we are just discussing terminology here. The following are equiavalent ways of saying the same thing:

• Type $B$ depends on type $A$
• $B$ is a type family indexed by type $A$
• $B$ is a dependent type indexed by type $A$
• $B : A \to \mathsf{Type}$
• for $x : A$, $B(x)$ is a type
• $x : A \vdash B(x) \ \mathsf{type}$

The reason we use the word family is that in mathematics a collection of sets indexed by a set, $\lbrace A_i \rbrace_{i \in I}$, is called a family of sets. It corresponds to a dependent type $A$ indexed by a type $I$.

• Some more terminology, for what it's worth. There is also a distinction between parameterized and indexed families of types. An excerpt from the Agda reference manual: The difference between an index and a parameter is that the index need not be constant throughout the definition of the type. The linked article has some examples illustrating the statement. – Anton Trunov Apr 5 '16 at 8:21
• @AntonTrunov: it is worth pointing out that the index/parameter terminology applies specifically to inductive datatypes, not to general types. In terms of fixed points, it is the difference between defining a family of types $B : A \to \mathsf{Type}$ as $\mu B : \mathsf{Type} . \lambda x : A . \cdots$ or $\lambda x : A . \mu B : \mathsf{Type} . \cdots$ – Andrej Bauer Apr 5 '16 at 9:06