The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Lee-Werner seem to lack coinductive types, modules, but also have:
Prop:Type0
However, Coq has:
Prop:Type1
https://coq.inria.fr/refman/Reference-Manual006.html

Lee-Werner observe that:
In this paper, we do not consider the sort Set. Indeed, when (the
impredicative or predicative sort)
Set is placed at the lowest level in the hierarchy of sorts, as in the
case of the current development of Coq, there is no way to provide a
universal set-theoretic interpretation of both Set and Prop, as
identified by [Reynolds(1984)].

On Fri, Jul 7, 2017 at 9:07 AM, Bas Spitters 
<b.a.w.spitters AT gmail.com>
 wrote:
> Thanks (I should have mentioned Bruno's work).
>
> It would be good to record these works and their limitations.
> I did not find an entry in cocorico, for instance.
>
> On Fri, Jul 7, 2017 at 9:02 AM, Amin Timany 
> <amintimany AT gmail.com>
>  wrote:
>> Hi Bas,
>>
>> It is indeed one of them. This paper establishes consistency by 
>> constructing
>> a set theoretic model and showing the interpretation of the type false is
>> indeed empty. Another one is  Bruno Barras’ habilitation
>> http://www.lix.polytechnique.fr/~barras/habilitation/. He proves strong
>> normalization for CIC and all proofs are also formalized Coq itself on top
>> of an axiomatization of IZF (Intuitionistic ZF).
>>
>> It should be noted though that these are not formalizing exactly what we in
>> Coq but they are pretty close. For example, if I’m not mistaken, neither of
>> them considers inductive types in Prop or eta expansion.
>>
>> Regards,
>> Amin
>>
>> On 7 Jul 2017, at 09:07, Bas Spitters 
>> <b.a.w.spitters AT gmail.com>
>>  wrote:
>>
>> https://coq.inria.fr/faq
>> "Proofs of consistency of *subsystems* of the theory of Coq can be
>> found in the literature."
>>
>> Is this what is intended?
>> Proof-irrelevant model of CC with predicative induction and judgmental
>> equality
>> Lee-Werner
>> https://arxiv.org/abs/1111.0123
>>
>> It might be good to add some references to the FAQ.
>>
>>