coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] True:Prop, True:Set and Prop vs Set

From: Georgi Guninski <guninski AT guninski.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] True:Prop, True:Set and Prop vs Set
Date: Wed, 6 Jul 2011 16:16:46 +0300
Header: best read with a sniffer

In 8.2 Prop=Set is provable by firstorder. This doesn't work in 8.3.

Yet all of this are provable in 8.3:
exists a : Set,a=True:Prop.
exists a : Prop,a=True:Prop.
exists! a : Type, a=True:Prop.

Is [Prop=Set] in 8.3 too ?

Definition FA := True:Prop.

Lemma set0: exists a : Set,a=FA.
eexists. firstorder.
Qed.

Lemma prop0: exists a : Prop,a=FA.
eexists. firstorder.
Qed.

Lemma typeuniq: exists! a : Type, a=FA.
eexists. firstorder.
Qed.

[Coq-Club] True:Prop, True:Set and Prop vs Set, Georgi Guninski
- Re: [Coq-Club] True:Prop, True:Set and Prop vs Set, Hugo Herbelin
  - Re: [Coq-Club] True:Prop, True:Set and Prop vs Set, Georgi Guninski
    - Re: [Coq-Club] True:Prop, True:Set and Prop vs Set, Hugo Herbelin