When we discuss some predicate in type theory, we are actually using the type $P$ from a universe $\cal U$ where $P$ becomes a term in the universe, or inhabitant. As its name, a dependent type means type dependent on a term, written $P(a): \cal U$ where $a$ is a term of $A$, meaning that the type $P(a)$ is dependent on $a:A$. Formally, $\Gamma, x: A \vdash P(x) : \cal U$.
Do note that $P(x)$ is not a function! If so, the type should be $A \to \mathcal{U}: \mathcal{U}$ which is self-contradictory: recall the Russels’ paradox. A set cannot contain itself (Impredicativity). A predicate with self-referential elements is impossible to deal with. The workaround is the introduction of hierarchy of the universe, which creates high-order logic systems. The thing is that we cannot have a sets of all sets; there are always “larger” sets.
Dependent types are useful in the context of computer-aided proofs. This is because if $\Gamma, x: A \vdash P(x) : \cal U$, we can derive some lovely properties for $x$ since types are predicates. This somehow reflects the first-order logic: we fix something $x$ and want to reason some propositions/theorems/lemmas on it. For example, we say if $n \in \mathbb{N}$ then $\mathrm{odd}(n) \vee \mathrm{even}(n)$. In this deduction, we indeed yet implicitly constructed a new type by $\Gamma, n : \mathbb{N} \vdash \mathrm{odd}(n) + \mathrm{even}(n) : \cal U.$
Universe Polymorphism
You cannot do $\mathcal{U}_i:\mathcal{U}_i$!!! So when you want polymorphism like this $id:(X: \mathcal{U}_i) \to X \to X$ we just cannot instantiate $X$ with $\mathcal{U}_i$. （自指命题 is impredicative）Can we just accept that universe is a type of the universe itself? Coq will automatically infer the type level but this is slow and may involve some sort of constraint solver.
The interesting thing (Carlo) is, can we “reverse” the universe instead of always going up that creates duplicate code snippet? Normally we will have $(\mathbb{N}, \le)$ but we can have $(\mathbb{Z}, \le)$, $(\mathbb{Q}, \le)$…
So to reason about polymorphism between universes, we can create a polymorphism $\cal H$ between the “level variable posets” formed by e.g., $\mathbb{Z}$ which is then embeded into the McBride monad $M = \Delta \times D$ where $D$ is an algebra for disreplacement that allows you to play with the levels you are interested in*.*
One might be confused with polymorphism when it comes to dependent type as they seem to be a similar notion.
Inductive my_list (a: Set): Set := ...
(* or *)
Inductive my_list': Set -> Set := ...
(* or *)
Inductive my_list'': forall (a: Set), Set := ...
Check my_list.
Check my_list'.
Check my_list''.
------------------
my_list*: Set -> Set.
Inductive my_list (n: nat): Set := ...
(* or *)
Inductive my_list': nat -> Set := ...
(* or *)
Inductive my_list'': forall _: nat, Set := ...
Check my_list.
Check my_list'.
Check my_list''.
------------------
my_list*: nat -> Set.
P.S.: Coq's forall is a dependent product type $\Pi_{a: Type} a \rightarrow \cal U$; You can think of the arrow as just syntactic sugar:
A -> B <===> forall _: A, B
For a real function $f$ defined on $[a,b] \subset \mathbb{R}$ we have:
$f$ is continuous on $[a,b]$ if and only if
$$ \forall x \in [a,b], \forall \varepsilon >0, \exists \delta > 0, \forall y \in [x,y], |y - x| < \delta \Rightarrow |f(y) - f(x)|<\varepsilon. $$
$f$ is uniformly continuous on $[a,b]$ if and only if
$$ \forall \varepsilon >0, \exists \delta > 0, \forall x,y \in [a,b], |x - y| < \delta \Rightarrow |f(x) - f(y)| < \varepsilon. $$
From Curry-Howard Correspondence, we know that types are predicates. Thus, we can rewrite the above judgment rules into:
$$ \Gamma, x: A, \varepsilon:B, \delta:C, y:A \vdash (|y - x| < \delta \Rightarrow |f(y) - f(x)| < \varepsilon) : \cal U. $$
We omit the second one for conciseness.