The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Hi. Some brief remarks:
(1) Benjamin Werner also treats the first question (when Set is 
impredicative), in his thesis;
however he only treats a truncated version of the Type hierarchy,
i.e. he has sorts Prop, Set and Type_1. Thus, technically speaking this 
doesn't answer the question for the case of
an arbitrary finite number of sorts Type_i (which is what Coq 
implements).  Also there are some differences between the
system he considers and the present version of Coq, notably the new 
eqT_rect and false_rect; and on the other hand he
treats eta-conversion which apparently is not implemented now. And on 
the whole it is already a lot of hard work!

(2) My understanding of the situation raised in the last paragraph is 
that Coq with Set predicative, is the same as just setting
Set := Type_0 (can anybody correct this if it is wrong?). Thus for Coq 
with Set predicative, Werner's paper treats the
question, perhaps modulo some minor details like explicit constructions 
of things he says are possible, and eqT_rect and false_rect.

(3) for the question about formulae in TT, to make it precise you would 
need to specify what is an allowable ``way of translating formulae into 
Coq''.

I would appreciate getting a CC of any emails on this subject which are 
not posted directly to coq_club...Thanks!
---Carlos Simpson