A new version of Hurkens.v.

Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs.

2 files changed, 349 insertions, 140 deletions

diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 34ae1cd5b..1a70f7806 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -367,7 +367,7 @@ Section Proof_irrelevance_EM_CC.
   Proof.
     refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H.
     trivial.
-    apply (paradox B p2b b2p (p2p2 H) p2p1).
+    apply (NoRetractFromSmallPropositionToProp.paradox B p2b b2p (p2p2 H) p2p1).
   Qed.
 
 End Proof_irrelevance_EM_CC.
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index d7871995c..903b91a59 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -8,22 +8,38 @@
 (*                              Hurkens.v                               *)
 (************************************************************************)
 
-(** Exploiting Hurkens' paradox [[Hurkens95]] for system U- so as to
-    derive contradictions from
-    - the existence in the pure Calculus of Constructions of a retract
-      from Prop into a small type of Prop
-    - the existence in the Calculus of Constructions with universes
-      of a retract from some Type universe into Prop
-
-    The first proof is a simple and effective formulation by Herman
-    Geuvers [[Geuvers01]] of a result by Thierry Coquand
-    [[Coquand90]]. The result implies that Coq with classical logic
-    stated in impredicative Set is inconsistent and that classical
-    logic stated in Prop implies proof-irrelevance (see
-    [ClassicalFacts.v])
-
-    The second proof is an adaptation of the first proof by Hugo
-    Herbelin to eventually prove the inconsistency of Prop=Type.
+(** Exploiting Hurkens's paradox [[Hurkens95]] for system U- so as to
+    derive various contradictory contexts.
+
+    The file is devided in various sub-modules which all follow the
+    same structure: a section introduce the contradictory hypotheses
+    and a theorem named [paradox] concludes the module with a proof of
+    [False].
+
+    - The [Generic] module contains the actual Hurkens's paradox for a
+      postulated shallow encoding of system U- in Coq. This is an
+      adaptation by Arnaud Spiwack of a previous, more restricted
+      implementation by Herman Geuvers. It is used to derive every
+      other special cases of the paradox in this file.
+
+    - The [NoRetractToImpredicativeUniverse] module contains a simple
+      and effective formulation by Herman Geuvers [[Geuvers01]] of a
+      result by Thierry Coquand [[Coquand90]]. It states that no
+      impredicative sort can contain a type of which it is a
+      retract. This result implies that Coq with classical logic
+      stated in impredicative Set is inconsistent and that classical
+      logic stated in Prop implies proof-irrelevance (see
+      [ClassicalFacts.v])
+
+    - The [NoRetractFromSmallPropositionToProp] module is a
+      specialisation of the [NoRetractToImpredicativeUniverse] module
+      to the case where the impredicative sort is [Prop].
+
+    - The [NoRetractFromTypeToProp] module proves that [Prop] cannot
+      be a retract of a larger type.
+
+    - The [Prop_neq_Type] module proves that [Prop] is different from
+      any larger [Type].
 
     References:
 
@@ -42,76 +58,306 @@
 
 (* Pleasing coqdoc! *)
 
-(** * Inconsistency of the existence in the pure Calculus of Constructions of a retract from Prop into a small type of Prop *)
 
-Module NoRetractFromSmallPropositionToProp.
+Set Universe Polymorphism.
+
+(** A modular proof of Hurkens's paradox. It relies on an
+    axiomatisation of a shallow embedding of system U- (i.e.  types of
+    U- are interepreted by types of Coq). The universes are encoding
+    in a style, due to Martin-Löf, where they are given with a set of
+    name and a family [El:Name->Type] which interprets each name into
+    a type. This allows the encoding of universe to be decoupled from
+    Coq's universes. Dependent products and abstractions are similarly
+    postulated rather than encoded as Coq's dependent products and
+    abstractions. *)
+
+Module Generic.
+
+(** Notations used in the proof. *)
+
+Reserved Notation "'∀₁' x : A , B" (at level 200, x ident, A at level 200,right associativity).
+Reserved Notation "A '⟶₁' B" (at level 99, right associativity, B at level 200).
+Reserved Notation "'λ₁' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "f '·₁' x" (at level 5, left associativity).
+Reserved Notation "'∀₂' A , F" (at level 200, A ident, right associativity).
+Reserved Notation "'λ₂' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "f '·₁' [ A ]" (at level 5, left associativity).
+Reserved Notation "'∀₀' x : A , B" (at level 200, x ident, A at level 200,right associativity).
+Reserved Notation "A '⟶₀' B" (at level 99, right associativity, B at level 200).
+Reserved Notation "'λ₀' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "f '·₀' x" (at level 5, left associativity).
+Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associativity).
+Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity).
 
 Section Paradox.
 
-(** Assumption of a retract from Prop to a small type in Prop, using
-    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).
-Variable B : Prop.
+(* arnaud: do some Coqdoc formatting *)
+(** Axiomatisation of impredicative universes in a Martin-Löf style *)
+
+(** System U- has two impredicative universes. In the proof of the
+    paradox they are slightly asymetric (in particular the reduction
+    rules of the small universe are not needed).  Therefore, the
+    axioms are duplicated allowing for a weaker requirement than the
+    actual system U-. *)
+
+
+(** Large universe *)
+Variable U1 : Type.
+Variable El1 : U1 -> Type.
+(** Closure by small product *)
+Variable Forall1 : forall u:U1, (El1 u -> U1) -> U1.
+  Notation "'∀₁' x : A , B" := (Forall1 A (fun x => B)).
+  Notation "A '⟶₁' B" := (Forall1 A (fun _ => B)).
+Variable lam1 : forall u B, (forall x:El1 u, El1 (B x)) -> El1 (∀₁ x:u, B x).
+  Notation "'λ₁' x , u" := (lam1 _ _ (fun x => u)).
+Variable app1 : forall u B (f:El1 (Forall1 u B)) (x:El1 u), El1 (B x).
+  Notation "f '·₁' x" := (app1 _ _ f x).
+Variable beta1 : forall u B (f:forall x:El1 u, El1 (B x)) x,
+                   (λ₁ y, f y) ·₁ x = f x.
+(** Closure by large products ([U1] only needs to quantify over itself) *)
+Variable ForallU1 : (U1->U1) -> U1.
+  Notation "'∀₂' A , F" := (ForallU1 (fun A => F)).
+Variable lamU1 : forall F, (forall A:U1, El1 (F A)) -> El1 (∀₂ A, F A).
+  Notation "'λ₂' x , u" := (lamU1 _ (fun x => u)).
+Variable appU1 : forall F (f:El1(∀₂ A,F A)) (A:U1), El1 (F A).
+  Notation "f '·₁' [ A ]" := (appU1 _ f A).
+Variable betaU1 : forall F (f:forall A:U1, El1 (F A)) A,
+                    (λ₂ x, f x) ·₁ [ A ] = f A.
+
+(** Small universe *)
+(** The small universe is an element of the large one. *)
+Variable u0 : U1.
+Notation U0 := (El1 u0).
+Variable El0 : U0 -> Type.
+(** Closure by small product, [U0] does not need reduction rules *)
+Variable Forall0 : forall u:U0, (El0 u -> U0) -> U0.
+  Notation "'∀₀' x : A , B" := (Forall0 A (fun x => B)).
+  Notation "A '⟶₀' B" := (Forall0 A (fun _ => B)).
+Variable lam0 : forall u B, (forall x:El0 u, El0 (B x)) -> El0 (∀₀ x:u, B x).
+  Notation "'λ₀' x , u" := (lam0 _ _ (fun x => u)).
+Variable app0 : forall u B (f:El0 (Forall0 u B)) (x:El0 u), El0 (B x).
+  Notation "f '·₀' x" := (app0 _ _ f x).
+(** Closure by large products *)
+Variable ForallU0 : forall u:U1, (El1 u->U0) -> U0.
+  Notation "'∀₀¹' A : U , F" := (ForallU0 U (fun A => F)).
+Variable lamU0 : forall U F, (forall A:El1 U, El0 (F A)) -> El0 (∀₀¹ A:U, F A).
+  Notation "'λ₀¹' x , u" := (lamU0 _ _ (fun x => u)).
+Variable appU0 : forall U F (f:El0(∀₀¹ A:U,F A)) (A:El1 U), El0 (F A).
+  Notation "f '·₀' [ A ]" := (appU0 _ _ f A).
+
+(** Automating the rewrite rules of our encoding. *)
+Local Ltac simplify :=
+  (* spiwack: ideally we could use [rewrite_strategy] here, but I am a tad
+     scared of the idea of depending on setoid rewrite in such a simple
+     file. *)
+  (repeat rewrite ?beta1, ?betaU1);
+  lazy beta.
+
+Local Ltac simplify_in h :=
+  (repeat rewrite ?beta1, ?betaU1 in h);
+  lazy beta in h.
+
+
+(** Hurkens's paradox. *)
+
+(** An inhabitant of [U0] standing for [False]. *)
+Variable F:U0.
+
+(** Preliminary definitions *)
+
+Definition V : U1 := ∀₂ A, ((A ⟶₁ u0) ⟶₁ A ⟶₁ u0) ⟶₁ A ⟶₁ u0.
+Definition U : U1 := V ⟶₁ u0.
+
+Definition sb (z:El1 V) : El1 V := λ₂ A, λ₁ r, λ₁ a, r ·₁ (z·₁[A]·₁r) ·₁ a.
+
+Definition le (i:El1 (U⟶₁u0)) (x:El1 U) : U0 :=
+  x ·₁ (λ₂ A, λ₁ r, λ₁ a, i ·₁ (λ₁ v, (sb v) ·₁ [A] ·₁ r ·₁ a)).
+Definition le' : El1 ((U⟶₁u0) ⟶₁ U ⟶₁ u0) := λ₁ i, λ₁ x, le i x.
+Definition induct (i:El1 (U⟶₁u0)) : U0 :=
+  ∀₀¹ x:U, le i x ⟶₀ i ·₁ x.
+
+Definition WF : El1 U := λ₁ z, (induct (z·₁[U] ·₁ le')).
+Definition I (x:El1 U) : U0 :=
+  (∀₀¹ i:U⟶₁u0, le i x ⟶₀ i ·₁ (λ₁ v, (sb v) ·₁ [U] ·₁ le' ·₁ x)) ⟶₀ F
+.
 
 (** Proof *)
 
-Definition V := forall A:Prop, ((A -> bool) -> A -> bool) -> A -> bool.
-Definition U := V -> bool.
-Definition sb (z:V) : V := fun A r a => r (z A r) a.
-Definition le (i:U -> bool) (x:U) : bool :=
-  x (fun A r a => i (fun v => sb v A r a)).
-Definition induct (i:U -> bool) : Prop :=
-  forall x:U, b2p (le i x) -> b2p (i x).
-Definition WF : U := fun z => p2b (induct (z U le)).
-Definition I (x:U) : Prop :=
-  (forall i:U -> bool, b2p (le i x) -> b2p (i (fun v => sb v U le x))) -> B.
-
-Lemma Omega : forall i:U -> bool, induct i -> b2p (i WF).
+Lemma Omega : El0 (∀₀¹ i:U⟶₁u0, induct i ⟶₀ i ·₁ WF).
 Proof.
-intros i y.
-apply y.
-unfold le, WF, induct.
-apply p2p2.
-intros x H0.
-apply y.
-exact H0.
+  refine (λ₀¹ i, λ₀ y, _).
+  refine (y·₀[_]·₀_).
+  unfold le,WF,induct. simplify.
+  refine (λ₀¹ x, λ₀ h0, _). simplify.
+  refine (y·₀[_]·₀_).
+  unfold le. simplify.
+  unfold sb at 1. simplify.
+  unfold le' at 1. simplify.
+  exact h0.
 Qed.
 
-Lemma lemma1 : induct (fun u => p2b (I u)).
+Lemma lemma1 : El0 (induct (λ₁ u, I u)).
 Proof.
-unfold induct.
-intros x p.
-apply (p2p2 (I x)).
-intro q.
-apply (p2p1 (I (fun v:V => sb v U le x)) (q (fun u => p2b (I u)) p)).
-intro i.
-apply q with (i := fun y => i (fun v:V => sb v U le y)).
+  unfold induct.
+  refine (λ₀¹ x, λ₀ p, _). simplify.
+  refine (λ₀ q,_).
+  assert (El0 (I (λ₁ v, (sb v)·₁[U]·₁le'·₁x))) as h.
+  { generalize (q·₀[λ₁ u, I u]·₀p). simplify.
+    intros q'.
+    exact q'. }
+  refine (h·₀_).
+  refine (λ₀¹ i,_).
+  refine (λ₀ h', _).
+  generalize (q·₀[λ₁ y, i ·₁ (λ₁ v, (sb v)·₁[U] ·₁ le' ·₁ y)]). simplify.
+  intros q'.
+  refine (q'·₀_). clear q'.
+  unfold le at 1 in h'. simplify_in h'.
+  unfold sb at 1 in h'. simplify_in h'.
+  unfold le' at 1 in h'. simplify_in h'.
+  exact h'.
 Qed.
 
-Lemma lemma2 : (forall i:U -> bool, induct i -> b2p (i WF)) -> B.
+Lemma lemma2 : El0 ((∀₀¹i:U⟶₁u0, induct i ⟶₀ i·₁WF) ⟶₀ F).
 Proof.
-intro x.
-apply (p2p1 (I WF) (x (fun u => p2b (I u)) lemma1)).
-intros i H0.
-apply (x (fun y => i (fun v => sb v U le y))).
-apply (p2p1 _ H0).
+  refine (λ₀ x, _).
+  assert (El0 (I WF)) as h.
+  { generalize (x·₀[λ₁ u, I u]·₀lemma1). simplify.
+    intros q.
+    exact q. }
+  refine (h·₀_). clear h.
+  refine (λ₀¹ i, λ₀ h0, _).
+  generalize (x·₀[λ₁ y, i·₁(λ₁ v, (sb v)·₁[U]·₁le'·₁y)]). simplify.
+  intros q.
+  refine (q·₀_). clear q.
+  unfold le in h0. simplify_in h0.
+  unfold WF in h0. simplify_in h0.
+  exact h0.
 Qed.
 
-Theorem paradox : B.
+Theorem paradox : El0 F.
 Proof.
-exact (lemma2 Omega).
+  exact (lemma2·₀Omega).
 Qed.
 
 End Paradox.
 
-End NoRetractFromSmallPropositionToProp.
+Ltac paradox h :=
+  refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ));cycle 1.
+
+End Generic.
+
+(** There can be no retract to an impredicative Coq universe from a
+    smaller type. In this version of the proof, the impredicativity of
+    the universe is postulated with a pair of functions from the
+    universe to its type and back which commute with dependent product
+    in an appropriate way. *)
+
+Module NoRetractToImpredicativeUniverse.
+
+Section Paradox.
+
+Let      U2    := Type.
+Let      U1:U2 := Type.
+Variable U0:U1.
+
+(** [U1] is impredicative *)
+Variable u22u1 : U2 -> U1.
+Hypothesis u22u1_unit   : forall (c:U2), c -> u22u1 c.
+(** [u22u1_counit] and [u22u1_coherent] only apply to dependent
+    product so that the equations happen in the smaller [U1] rather
+    than [U2].  Indeed, it is not generally the case that one can
+    project from a large universe to an impredicative universe and
+    then get back the original type again. It would be too strong a
+    hypothesis to require (in particular, it is not true of
+    [Prop]). The formulation is reminiscent of the monadic
+    characteristic of the projection from a large type to [Prop].*)
+Hypothesis u22u1_counit : forall (F:U1->U1), u22u1 (forall A,F A) -> (forall A,F A).
+Hypothesis u22u1_coherent : forall (F:U1 -> U1) (f:forall x:U1, F x) (x:U1), 
+                              u22u1_counit _ (u22u1_unit _ f) x = f x.
+
+(** [U0] is a retract of [U1] *)
+Variable u02u1 : U0 -> U1.
+Variable u12u0 : U1 -> U0.
+Hypothesis u12u0_unit   : forall (b:U1), b -> u02u1 (u12u0 b).
+Hypothesis u12u0_counit : forall (b:U1), u02u1 (u12u0 b) -> b.
+
+(** Paradox *)
+
+Theorem paradox : forall F:U1, F.
+Proof.
+  intros F.
+  Generic.paradox h.
+  (** Large universe *)
+  + exact U1.
+  + exact (fun X => X).
+  + cbn. exact (fun u F => forall x:u, F x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. easy.
+  + cbn. exact (fun F => u22u1 (forall x, F x)).
+  + cbn. exact (fun _ x => u22u1_unit _ x).
+  + cbn. exact (fun _ x => u22u1_counit _ x).
+  + cbn. intros **. now rewrite u22u1_coherent.
+  (** Small universe *)
+  + exact U0.
+  (** The interpretation of the small universe is the image of
+      [U0] in [U1]. *)
+  + cbn. exact (fun X => u02u1 X).
+  + cbn. exact (fun u F => u12u0 (forall x:(u02u1 u), u02u1 (F x))).
+  + cbn. intros * x. exact (u12u0_unit _ x).
+  + cbn. intros * x. exact (u12u0_counit _ x).
+  + cbn. exact (fun u F => u12u0 (forall x:u, u02u1 (F x))).
+  + cbn. intros * x. exact (u12u0_unit _ x).
+  + cbn. intros * x. exact (u12u0_counit _ x).
+  + cbn. exact (u12u0 F).
+  + cbn in h.
+    exact (u12u0_counit _ h).
+Qed.
+
+End Paradox.
+
+End NoRetractToImpredicativeUniverse.
+
+
+(** * Inconsistency of the existence in the pure Calculus of Constructions of a retract from Prop into a small type of Prop *)
+
+Module NoRetractFromSmallPropositionToProp.
+
+Section Paradox.
+
+(** Assumption of a retract from Prop to a small type in Prop, using *)
+(*     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).
 
-Export NoRetractFromSmallPropositionToProp.
+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.
 
 (** * Inconsistency of the existence in the Calculus of Constructions with universes of a retract from some Type universe into Prop. *)
 
@@ -127,85 +373,44 @@ Definition Type1 := Type : Type2.
 
 Section Paradox.
 
-Notation "'rew1' <- H 'in' H'" := (@eq_rect_r Type1 _ (fun X : Type1 => X) H' _ H)
-    (at level 10, H' at level 10).
-Notation "'rew1' H 'in' H'" := (@eq_rect Type1 _ (fun X : Type1 => X) H' _ H)
-    (at level 10, H' at level 10).
-
 (** Assumption of a retract from Type into Prop *)
 
 Variable down : Type1 -> Prop.
 Variable up : Prop -> Type1.
 Hypothesis up_down : forall (A:Type1), up (down A) = A :> Type1.
 
-(** Proof *)
-
-Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop.
-Definition U : Type1 := V -> Prop.
-
-Definition forth (a:U) : up (down U) := rew1 <- (up_down U) in a.
-Definition back (x:up (down U)) : U := rew1 (up_down U) in x.
-
-Definition sb (z:V) : V := fun A r a => r (z A r) a.
-Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)).
-Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth a)) (back x).
-Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x).
-Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth a))).
-Definition I (x:U) : Prop :=
-  (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth x)))) -> False.
-
-Lemma back_forth (a:U) : back (forth a) = a.
+Theorem paradox : forall P:Prop, P.
 Proof.
-apply rew_opp_r with (P:=fun X:Type1 => X).
-Defined.
-
-Lemma Omega : forall i:U -> Prop, induct i -> up (i WF).
-Proof.
-intros i y.
-apply y.
-unfold le, WF, induct.
-rewrite up_down.
-intros x H0.
-apply y.
-unfold sb, le', le.
-rewrite back_forth.
-exact H0.
-Qed.
-
-Lemma lemma1 : induct (fun u => down (I u)).
-Proof.
-unfold induct.
-intros x p.
-rewrite up_down.
-intro q.
-generalize (q (fun u => down (I u)) p).
-rewrite up_down.
-intro r.
-apply r.
-intros i j.
-unfold le, sb, le', le in j |-.
-rewrite back_forth in j.
-specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth y))).
-apply q.
-exact j.
-Qed.
-
-Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False.
-Proof.
-intro x.
-generalize (x (fun u => down (I u)) lemma1).
-rewrite up_down.
-intro r. apply r.
-intros i H0.
-apply (x (fun y => i (fun v => sb v (down U) le' (forth y)))).
-unfold le, WF in H0.
-rewrite up_down in H0.
-exact H0.
-Qed.
-
-Theorem paradox : False.
-Proof.
-exact (lemma2 Omega).
+  intros P.
+  Generic.paradox h.
+  (** Large universe. *)
+  + exact Type1.
+  + exact (fun X => X).
+  + cbn. exact (fun u F => forall x, F x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. easy.
+  + exact (fun F => forall A:Prop, F(up A)).
+  + cbn. exact (fun F f A => f (up A)).
+  + cbn.
+    intros F f A.
+    specialize (f (down A)).
+    rewrite up_down in f.
+    exact f.
+  + cbn.
+    intros F f A.
+    destruct (up_down A). cbn.
+    reflexivity.
+  + exact Prop.
+  + cbn. exact (fun X => X).
+  + cbn. exact (fun A P => forall x:A, P x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun A P => forall x:A, P x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact P.
+  + exact h.
 Qed.
 
 End Paradox.
@@ -214,9 +419,11 @@ End NoRetractFromTypeToProp.
 
 (** Application: Prop<>Type for some given Type *)
 
+Module PropNeqType.
+
 Import NoRetractFromTypeToProp.
 
-Section Prop_neq_Type.
+Section Paradox.
 
 Notation "'rew2' <- H 'in' H'" := (@eq_rect_r Type2 _ (fun X : Type2 => X) H' _ H)
     (at level 10, H' at level 10).
@@ -233,10 +440,12 @@ Proof.
 unfold up, down. rewrite Heq. reflexivity.
 Defined.
 
-Theorem Prop_neq_Type : False.
+Theorem paradox : False.
 Proof.
 apply paradox with down up.
 apply up_down.
 Qed.
 
-End Prop_neq_Type.
+End Paradox.
+
+End PropNeqType.