aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-09-18 20:39:34 +0200
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-09-24 12:25:55 +0200
commite8e994afb5a29f92c750fb370d01b704ddf06cc4 (patch)
treeb971d0e9083c049c5fd0058bf316c4972589744a /theories/Logic
parent2739fe8a22a9df48e717583d6efabc42e41f9814 (diff)
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.
Diffstat (limited to 'theories/Logic')
-rw-r--r--theories/Logic/ClassicalFacts.v2
-rw-r--r--theories/Logic/Hurkens.v487
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.