diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-23 11:11:08 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-24 12:25:55 +0200 |
commit | 4ca7900108f5b6d713b8d1c34afab284423bae65 (patch) | |
tree | 475639dcd46ac10143c0d9fb492e22502031b9b6 /theories/Logic | |
parent | 926e25e8e9905e1ebbdbefc7ea3c8474cb523ec4 (diff) |
Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].
Diffstat (limited to 'theories/Logic')
-rw-r--r-- | theories/Logic/Hurkens.v | 90 |
1 files changed, 75 insertions, 15 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index ab50d7c48..3111c7351 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -435,35 +435,95 @@ End Paradox. End NoRetractFromTypeToProp. -(** * [Prop<>Type]. *) +(** * [A<>Type] *) -Module PropNeqType. +(** No Coq universe can be equal to one of its elements. *) -Import NoRetractFromTypeToProp. +Module TypeNeqSmallType. Section Paradox. -Notation "'rew2' <- H 'in' H'" := (@eq_rect_r Type2 _ (fun X : Type2 => X) H' _ H) - (at level 10, H' at level 10). -Notation "'rew2' H 'in' H'" := (@eq_rect Type2 _ (fun X : Type2 => X) H' _ H) - (at level 10, H' at level 10). +(** ** Universe [U] is equal to one of its elements. *) + +Let U := Type. +Variable A:U. +Hypothesis h : U=A. + +(** ** Universe [U] is a retract of [A] *) -Variable Heq : Prop = Type1 :> Type2. +(** The following context is actually sufficient for the paradox to + hold. The hypothesis [h:U=A] is only used to define [down], [up] + and [up_down]. *) -Definition down : Type1 -> Prop := fun A => rew2 <- Heq in A. -Definition up : Prop -> Type1 := fun A => rew2 Heq in A. +Let down (X:U) : A := @eq_rect _ _ (fun X => X) X _ h. +Let up (X:A) : U := @eq_rect_r _ _ (fun X => X) X _ h. -Lemma up_down : forall (A:Type1), up (down A) = A :> Type1. +Lemma up_down : forall (X:U), up (down X) = X. Proof. -unfold up, down. rewrite Heq. reflexivity. -Defined. + unfold up,down. + rewrite <- h. + reflexivity. +Qed. + Theorem paradox : False. Proof. -apply paradox with down up. -apply up_down. + Generic.paradox p. + (** Large universe *) + + exact U. + + exact (fun X=>X). + + cbn. exact (fun X F => forall x:X, F x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + cbn. easy. + + exact (fun F => forall x:A, F (up x)). + + cbn. exact (fun _ f => fun x:A => f (up x)). + + cbn. intros * f X. + specialize (f (down X)). + rewrite up_down in f. + exact f. + + cbn. intros ? f X. + destruct (up_down X). cbn. + reflexivity. + (** Small universe *) + + exact A. + (** The interpretation of [A] as a universe is [U]. *) + + cbn. exact up. + + cbn. exact (fun _ F => down (forall x, up (F x))). + + cbn. intros ? ? f. + rewrite up_down. + exact f. + + cbn. intros ? ? f. + rewrite up_down in f. + exact f. + + cbn. exact (fun _ F => down (forall x, up (F x))). + + cbn. intros ? ? f. + rewrite up_down. + exact f. + + cbn. intros ? ? f. + rewrite up_down in f. + exact f. + + cbn. exact (down False). + + rewrite up_down in p. + exact p. Qed. End Paradox. +End TypeNeqSmallType. + +(** * [Prop<>Type]. *) + +(** Special case of [TypeNeqSmallType]. *) + +Module PropNeqType. + +Theorem paradox : Prop <> Type. +Proof. + intros h. + refine (TypeNeqSmallType.paradox _ _). + + exact Prop. + + easy. +Qed. + End PropNeqType. |