Extension type

[jonsterling]

No description provided.

[jonsterling]

I have decided that rather than try and implement a modality for just this purpose, we will special-case it in the following way:

(* Syntax *)
type t =
...
| Ext of {len : nat; cof : [`Global of t]; cube : t; part : t}
...

(* Semantics *)
type con =
...
| Ext of {len : nat; cof : [`Global of cof]; cube : con; part : con}
...

The cof argument is a global element of (psi : dim^len) -> cof; the de Bruijn index counting convention is un-altered (since those count from the right), but we must evaluate cof in a completely empty environment. Likewise, we must elaborate it in a completely empty environment.

The cube argument is a cube of type codes, as always. The part argument is a partial cube of elements --- whose support is the appropriate weakening of cof. However, because weakening is implicit in the semantic domain, we can do this totally seamlessly.

---

unfold_el will take the extension type code to a bunch of dependent product and cubical subtype.

[favonia]

This looks great. tp seems better than cube to me, though. Also, shouldn't we try to remember the variable names somewhere?

[jonsterling]

The variable names can be remembered in the lambdas that get put under those constructors.