type

Type

A type is a set $T$.
A typed element is a pair $(x,T),x\in T$; also written as $(x:T)$.
A typed function $f$ has a specified domain (input type) and codomain (output type): $f:A\to B$
A typing on an index set $I$ is a map $T:I\to \text{Set},i\mapsto T(i)=T_i$, assigning to each index $i$ a set $T_i$ (its type). Note: this is just an $I$-indexed family of sets $\{T_i{\}}_{i\in I}$
A typed family is a family $\{x_i{\}}_{i\in I}$ of elements $x_i\in T_i$, i.e. a function $x:I\to {\bigcup }_{i\in I}{T}_i,i\mapsto x(i)=x_i\in T_i$.

EXAMPLE

$(3,\mathbb{Z})$ is a typed element of type $\mathbb{Z}$.
$f:\mathbb{R}\to \mathbb{R},x\mapsto x^2$ is a typed function with domain and codomain $\mathbb{R}$.
$I=\{\text{name, age}\}$, a typing could be $T(\text{name})=\text{String}=T_{\text{name}}$, $T(\text{age})=\mathbb{N}=T_{\text{age}}$.