OTT by reflecting telescopes
Monday, May 16th, 2005Starting 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
(more…)