Non-dependant PTS's

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

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.

Thanks in advance

Neil Ghani 

Tel	+33 1 44 32 32 77
Email	ghani@ens.fr
Webress	http://www.ens.fr/~ghani 
Address ENS, 45 Rue D'Ulm, 75230 Paris Cedex 05, France