OTT by reflecting telescopes

Starting point: TT with some proper dependency, e.g.

b : Bool
————–
T b : *

T false = Null
T true = One

we assume at least Pi, Sigma, Empty, Null, One, Bool. We also use Prop <= *,
for propositional types.

We introduce telescopes G |- D Tel , e.g.

-----------
G |- () Tel

G |- D Tel G.D |- S : *
-----------------------------
G |- D.S Tel

where

G.() = G
G.(D.S) = (G.D).S

We inhabit telescopes with substitutions, given G |- D Tel

G |- ts : D

and at the same time define

G.D |- A
——————
G |- let D=ts in A

G.D |- t : A
———————————-
G |- let D=ts in t : let D=ts in A

To simplify the presentation, we reflect telescopes back as types and substitutions as terms, i.e. given G |- D Tel we define G |- |D| : * using Sigma and Unit. We also reflect families over telescopes, i.e. given G.D |- S : * we define G.x:|D| |- |S| x : *

[To close the knot I have to reflect back as well...]

Now we are able to reflect important aspects of the setoid model (using JM equality):
We define

G |- D Tel G |- d,d’ : |D|
——————————-
G |- Eq d d’ : Prop

tgether with refl,sym,trans. Next we introduce equality for families:

G |- D Tel G |- d,d’ : |D|
G |- p : Eq d d’
G.D |- S
G |- x : |S| d
G |- y : |S| d’
————————————
G |- Eqq p x y : Prop

together with JM-versions of refl, sym, trans and the substitution operator:

G |- D Tel G |- d,d’ : |D|
G |- p : Eq d d’
G.D |- S
G |- x : |S| d
———————————–
G |- subst S p x : |S| d’
G |- subst-eq S p x : Eqq p (subst S p x) x

Does this work?
Is there a cooler way?

Yes, I know, I have ignored the reflexivity optimisation issue in the moment.

Leave a Reply