Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Prop : Prop should not work #35

Closed
JasonGross opened this issue May 1, 2013 · 1 comment
Closed

Prop : Prop should not work #35

JasonGross opened this issue May 1, 2013 · 1 comment

Comments

@JasonGross
Copy link 

Check Prop : Prop. (* Prop:Prop
     : Prop *)
Check Set : Prop. (* Set:Prop
     : Prop *)
Check ((bool -> Prop) : Prop). (* bool -> Prop:Prop
     : Prop *)
Axiom proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.
Check ((True : Prop) : Set). (* (True:Prop):Set
     : Set *)
Goal (forall (v : Type) (f1 f0 : v -> Prop),
        @eq (v -> Prop) f0 f1).
intros.
apply proof_irrelevance.
Defined. (* Unnamed_thm is defined *)
Set Printing Universes.
Check ((True : Prop) : Set). (* Toplevel input, characters 0-28:
Error: Universe inconsistency (cannot enforce Prop <= Set because Set
< Prop). *)
mattam82 added a commit that referenced this issue May 2, 2013
@mattam82
Fix bug spotted in issue #35, now treating Prop/Set specially as rigi…
c74db8e 
…d universes

that can't be identified.
mattam82 added a commit that referenced this issue May 8, 2013
@mattam82
Fix [change] forgeting about universes in the right-hand-side (#36) a…
3745dba 
…nd better fix for #35 and #37,

disallowing only Set/Set+1 <= Prop constraints.
@JasonGross
Copy link
Author

This has been fixed.

JasonGross added a commit to CategoricalData/catdb that referenced this issue Jan 28, 2015
@JasonGross
Work around another bug in HoTT/coq
5a6d776 
HoTT/coq#35

`Prop : Prop` should not work

Check Prop : Prop. (* Prop:Prop
     : Prop *)
Check Set : Prop. (* Set:Prop
     : Prop *)
Check ((bool -> Prop) : Prop). (* bool -> Prop:Prop
     : Prop *)
Axiom proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.
Check ((True : Prop) : Set). (* (True:Prop):Set
     : Set *)
Goal (forall (v : Type) (f1 f0 : v -> Prop),
        @eq (v -> Prop) f0 f1).
intros.
apply proof_irrelevance.
Defined. (* Unnamed_thm is defined *)
Set Printing Universes.
Check ((True : Prop) : Set). (* Toplevel input, characters 0-28:
Error: Universe inconsistency (cannot enforce Prop <= Set because Set
< Prop). *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@JasonGross