Merge branch 'v8.5'

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