Idris2Doc : Data.Rel

Data.Rel

All : (ts : Vectn Type) -> Relts -> Type
Universal quantification of a n-ary Relation over its
arguments to build a (function) type from a `Rel` type

```
λ> All [Nat,Nat] LTE
(x : Nat) -> (x : Nat) -> LTE x x
```
Ex : (ts : Vectn Type) -> Relts -> Type
Existential quantification of a n-ary relation over its
arguments to build a dependent pair (eg. Sigma type).

Given a (type of) relation `p : [t_1, t_2 ... t_n] x r` where `t_i` and `r` are
types, `Ex` builds the type `Σ (x_1 : t_1). Σ (x_2 : t_2) ... . r`
For example:
```
λ> Ex [Nat,Nat] LTE
(x : Nat ** (x : Nat ** LTE x x))
```
Which is the type of a pair of natural numbers along with a proof that the first
is smaller or equal than the second.
Rel : Vectn Type -> Type
Build an n-ary relation type from a Vect of Types
liftRel : (ts : Vectn Type) -> Relts -> (Type -> Type) -> Type
Map a type-level function over the co-domain of a n-ary Relation