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.