Univs: entirely disallow instantiation of polymorphic constants with

Prop levels.

As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.

2 files changed, 74 insertions, 48 deletions

diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 6f736e45f..cdc3e0461 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -658,4 +658,3 @@ Proof.
     exists x; intro; exact Hx.
     exists x0; exact Hnot.
 Qed.
-
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index ede51f57f..4e582934a 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -344,53 +344,6 @@ End Paradox.
 
 End NoRetractToImpredicativeUniverse.
 
-(** * Prop is not a retract *)
-
-(** The existence in the pure Calculus of Constructions of a retract
-    from [Prop] into a small type of [Prop] is inconsistent. This is a
-    special case of the previous result. *)
-
-Module NoRetractFromSmallPropositionToProp.
-
-Section Paradox.
-
-(** ** Retract of [Prop] in a small type *)
-
-(** The retract is axiomatized using logical equivalence as the
-    equality on propositions. *)
-
-Variable bool : Prop.
-Variable p2b : Prop -> bool.
-Variable b2p : bool -> Prop.
-Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
-Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
-
-(** ** Paradox *)
-
-Theorem paradox : forall B:Prop, B.
-Proof.
-  intros B.
-  pose proof
-      (NoRetractToImpredicativeUniverse.paradox@{Type Prop}) as P.
-  refine (P _ _ _ _ _ _ _ _ _ _);clear P.
-  + exact bool.
-  + exact (fun x => forall P:Prop, (x->P)->P).
-  + cbn. exact (fun _ x P k => k x).
-  + cbn. intros F P x.
-    apply P.
-    intros f.
-    exact (f x).
-  + cbn. easy.
-  + exact b2p.
-  + exact p2b.
-  + exact p2p2.
-  + exact p2p1.
-Qed.
-
-End Paradox.
-
-End NoRetractFromSmallPropositionToProp.
-
 (** * Modal fragments of [Prop] are not retracts *)
 
 (** In presence of a a monadic modality on [Prop], we can define a
@@ -534,6 +487,80 @@ End Paradox.
 
 End NoRetractToNegativeProp.
 
+(** * Prop is not a retract *)
+
+(** The existence in the pure Calculus of Constructions of a retract
+    from [Prop] into a small type of [Prop] is inconsistent. This is a
+    special case of the previous result. *)
+
+Module NoRetractFromSmallPropositionToProp.
+
+(** ** The universe of propositions. *)
+
+Definition NProp := { P:Prop | P -> P}.
+Definition El : NProp -> Prop := @proj1_sig _ _.
+
+Section MParadox.
+
+(** ** Retract of [Prop] in a small type, using the identity modality. *)
+
+Variable bool : NProp.
+Variable p2b : NProp -> El bool.
+Variable b2p : El bool -> NProp.
+Hypothesis p2p1 : forall A:NProp, El (b2p (p2b A)) -> El A.
+Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
+
+(** ** Paradox *)
+
+Theorem mparadox : forall B:NProp, El B.
+Proof.
+  intros B.
+  refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+  + exact (fun P => P).
+  + cbn. auto.
+  + cbn. auto.
+  + cbn. auto.
+  + exact bool.
+  + exact p2b.
+  + exact b2p.
+  + auto.
+  + auto.
+  + exact B.
+  + exact h.
+Qed.
+
+End MParadox.
+
+Section Paradox.
+
+(** ** Retract of [Prop] in a small type *)
+
+(** The retract is axiomatized using logical equivalence as the
+    equality on propositions. *)
+Variable bool : Prop.
+Variable p2b : Prop -> bool.
+Variable b2p : bool -> Prop.
+Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
+Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
+
+(** ** Paradox *)
+
+Theorem paradox : forall B:Prop, B.
+Proof.
+  intros B.
+  refine (mparadox (exist _ bool (fun x => x)) _ _ _ _
+                   (exist _ B (fun x => x))).
+  + intros p. red. red. exact (p2b (El p)).
+  + cbn. intros b. red. exists (b2p b). exact (fun x => x).
+  + cbn. intros [A H]. cbn. apply p2p1.
+  + cbn. intros [A H]. cbn. apply p2p2.
+Qed.
+
+End Paradox.
+
+End NoRetractFromSmallPropositionToProp.
+
+
 (** * Large universes are no retracts of [Prop]. *)
 
 (** The existence in the Calculus of Constructions with universes of a