[Prev][Next][Index][Thread]
Re: Non-dependant PTS's
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
Neil Ghani asks:
> Has there been any work on generalising the translation of the
> Calculus of Constructions into Fw to a more abstract setting. Say
> for instance where one has a notion of what a "non-dependant" PTS is
> and then for every PTS one selects a (as large as possible)
> non-dependant sub-PTS and shows that a translation exists.
The same projection works for the whole lambda cube, taking the right
plane into the left plane. (See Geuvers' thesis for details; the
projection for the lambda cube is described on p.153.) This is
usually attributed independently to Christine Paulin and Stefano
Berardi, and the same idea was used by Furio Honsell about the same
time to prove SN for the Edinburgh Logical Framework.
Knowing Geuvers' observation that Fomega with one universe is
isomorphic to (Intuitionistic, Minimal) HOL, Luo extended this
projection to map ECC into Fomega with universes, giving a
conservative embedding of HOL into CC with one universe, in contrast
to the non-conservativity of the embedding of HOL into CC that
confuses the type of individuals with the type of propositions (this
latter observed by Geuvers and Berardi). (Also compare with the
solution in Coq of splitting the Prop level.)
Best wishes,
Randy Pollack