Girard's System F have the following definition for natural numbers : $$ \mathbb N := \forall\alpha, (\alpha\rightarrow\alpha) \rightarrow (\alpha\rightarrow\alpha) $$
A dependent type system can have a similar definition based on dependent product (where $\mathbb T$ is the type of all types) : $$ \mathbb N := \prod_{\alpha:\mathbb T} (\alpha\rightarrow\alpha) \rightarrow (\alpha\rightarrow\alpha) $$
Let's define the $\lambda$-term successor in this dependent type system : $$ S := \lambda n^{\mathbb N}. \lambda\alpha^{\mathbb T}. \lambda s^{\alpha\rightarrow\alpha}. \lambda z^\alpha. s \bigl( n \alpha s z \bigr) $$
We know that relation $\leq$ on natural numbers satisfies the following first order logic propositions : $$ \forall m, \forall n, m \leq n \Rightarrow m \leq S n $$ $$ \forall n, n \leq n $$
Can we define $\leq$ in our dependent type system like we defined $\mathbb N$ ? : $$ \leq := \prod_{p:\mathbb N} \prod_{q:\mathbb N} \prod_{\alpha:\mathbb N\rightarrow(\mathbb N\rightarrow\mathbb T)} \bigl( \prod_{m:\mathbb N} \prod_{n:\mathbb N} (\alpha m n) \rightarrow (\alpha m (S n)) \bigr) \rightarrow \bigl( \prod_{x:\mathbb N} \alpha x x \bigr) \rightarrow (\alpha p q) $$
Or : $$ \leq := \sum_{p:\mathbb N} \prod_{q:\mathbb N} \prod_{\alpha:\mathbb N\rightarrow(\mathbb N\rightarrow\mathbb T)} \bigl( \prod_{m:\mathbb N} \prod_{n:\mathbb N} (\alpha m n) \rightarrow (\alpha m (S n)) \bigr) \rightarrow \bigl( \prod_{x:\mathbb N} \alpha x x \bigr) \rightarrow (\alpha p q) $$
Night was helpful, I think I found the right definition : $$ \leq := \lambda p^{\mathbb N}. \lambda q^{\mathbb N}. \Biggl( \prod_{\alpha:\mathbb N\rightarrow(\mathbb N\rightarrow\mathbb T)} \bigl( \prod_{m:\mathbb N} \prod_{n:\mathbb N} (\alpha m n) \rightarrow (\alpha m (S n)) \bigr) \rightarrow \bigl( \prod_{x:\mathbb N} \alpha x x \bigr) \rightarrow (\alpha p q) \Biggr) $$