Data.Telescope.Segment

A segment is a compositional fragment of a telescope.
A key difference is that segments are right-nested, whereas
telescopes are left nested.
So telescopes are convenient for well-bracketing dependencies,
but segments are convenient for processing telescopes from left
to right.

As with telescopes, indexing segments by their length (hopefully)
helps the type-checker infer stuff.

Definitions

data Segment : Nat -> Telescope k -> Type

  A segment is a compositional fragment of a telescope, indexed by
  the segment's length.

Totality: total
Visibility: public export
Constructors:

Nil : Segment 0 gamma

(::) : (ty : TypeIn gamma) -> Segment n (gamma -. ty) -> Segment (S n) gamma

tabulate : (n : Nat) -> (Environment gamma -> Telescope n) -> Segment n gamma

  A segment of size `n` indexed by `gamma` can be seen as the tabulation of a
  function that turns environments for `gamma` into telescopes of size `n`.

Totality: total
Visibility: public export

fromTelescope : Telescope k -> Segment k []

  Any telescope is a segment in the empty telescope. It amounts to looking
  at it left-to-right instead of right-to-left.

Totality: total
Visibility: public export

untabulate : Segment n gamma -> Environment gamma -> Telescope n

  Conversely, a segment of size `n` in telescope `gamma` can be seen as a function
  from environments for `gamma` to telescopes of size `n`.

Totality: total
Visibility: public export

toTelescope : Segment k [] -> Telescope k

  Any segment in the empty telescope correspond to a telescope.

Totality: total
Visibility: public export

keep : (0 _ : a = b) -> a = b

Totality: total
Visibility: public export

(|++) : (gamma : Telescope k) -> Segment n gamma -> Telescope (n + k)

  Segments act on telescope from the right.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3

(++) : (lft : Segment n gamma) -> Segment m (gamma |++ lft) -> Segment (n + m) gamma

  Segments form a kind of an indexed monoid w.r.t. the action `(|++)`

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

actSegmentAssociative : (gamma : Telescope k) -> (lft : Segment n gamma) -> (rgt : Segment m (gamma |++ lft)) -> gamma |++ (lft ++ rgt) = (gamma |++ lft) |++ rgt

Totality: total
Visibility: export

weaken : TypeIn gamma -> TypeIn (gamma |++ delta)

Totality: total
Visibility: public export

projection : Environment (gamma |++ delta) -> Environment gamma

Totality: total
Visibility: public export

data Environment : Environment gamma -> Segment n gamma -> Type

Totality: total
Visibility: public export
Constructors:

Empty : Environment env []

(.=) : (x : ty env) -> Environment (env ** x) delta -> Environment env (ty :: delta)

(:++) : (env : Environment gamma) -> Environment env delta -> Environment (gamma |++ delta)

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3