0 | ||| A telescope is the variable context in a dependently typed program.
 1 | ||| Dependent types with free variables  are really only well-defined in a telescope.
 2 | |||
 3 | ||| A segment of a telescope is a tuple of types in that
 4 | ||| telescope. These are usually implicit in formal developments, but
 5 | ||| seem to be crucial to get a compositional account. Here we use
 6 | ||| them to get 'n-ary dependent function' (compare with `Data.Fun`
 7 | ||| and `Data.Rel`).
 8 | |||
 9 | ||| I've learned this from Conor McBride on an SPLV'19 bus ride.
10 | ||| A literary reference would be welcome. This paper is a start:
11 | ||| Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data.
12 | ||| Jesper Cockx, Dominique Devriese, Frank Piessens, ICFP'16.
13 | ||| but they don't seem to have segments and their left action on contexts.
14 | module Data.Telescope
15 |
16 | import public Data.Telescope.Telescope
17 | import public Data.Telescope.Segment
18 | import public Data.Telescope.SimpleFun
19 | import public Data.Telescope.Fun
20 | import public Data.Telescope.Congruence
21 |