coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Carlos.SIMPSON" <carlos AT math.unice.fr>
- To: "Robert M. Solovay" <solovay AT Math.Berkeley.EDU>
- Cc: Coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Some metatheoretical questions re Coq
- Date: Mon, 13 Sep 2004 13:54:42 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] Some metatheoretical questions re Coq, Robert M. Solovay
- Re: [Coq-Club] Some metatheoretical questions re Coq, Carlos.SIMPSON
- Re: [Coq-Club] Some metatheoretical questions re Coq, Robert M. Solovay
- Re: [Coq-Club] Some metatheoretical questions re Coq, Benjamin Werner
- Re: [Coq-Club] Some metatheoretical questions re Coq, Carlos.SIMPSON
Archive powered by MhonArc 2.6.16.