0 | module Data.Rel
 1 |
 2 | import Data.Fun
 3 |
 4 | %default total
 5 |
 6 | ||| Build an n-ary relation type from a Vect of Types
 7 | public export
 8 | Rel : Vect n Type -> Type
 9 | Rel ts = Fun ts Type
10 |
11 | ||| Universal quantification of a n-ary Relation over its
12 | ||| arguments to build a (function) type from a `Rel` type
13 | |||
14 | ||| ```
15 | ||| λ> All [Nat,Nat] LTE
16 | ||| (x : Nat) -> (x : Nat) -> LTE x x
17 | ||| ```
18 | public export
19 | All : (ts : Vect n Type) -> (p : Rel ts) -> Type
20 | All [] p = p
21 | All (t :: ts) p = (x : t) -> All ts (p x)
22 |
23 | ||| Existential quantification of a n-ary relation over its
24 | ||| arguments to build a dependent pair (eg. Sigma type).
25 | |||
26 | ||| Given a (type of) relation `p : [t_1, t_2 ... t_n] x r` where `t_i` and `r` are
27 | ||| types, `Ex` builds the type `Σ (x_1 : t_1). Σ (x_2 : t_2) ... . r`
28 | ||| For example:
29 | ||| ```
30 | ||| λ> Ex [Nat,Nat] LTE
31 | ||| (x : Nat ** (x : Nat ** LTE x x))
32 | ||| ```
33 | ||| Which is the type of a pair of natural numbers along with a proof that the first
34 | ||| is smaller or equal than the second.
35 | public export
36 | Ex : (ts : Vect n Type) -> (p : Rel ts) -> Type
37 | Ex [] p = p
38 | Ex (t :: ts) p = (x : t ** Ex ts (p x))
39 |
40 | ||| Map a type-level function over the co-domain of a n-ary Relation
41 | public export
42 | liftRel : (ts : Vect n Type) -> (p : Rel ts) -> (Type -> Type) -> Type
43 | liftRel ts p f = All ts $ map @{Nary} f p
44 |