# How to define inferiority relation on natural numbers in a dependently typed lambda-calculus?

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)$$