diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-21 11:55:32 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:10 +0200 |
| commit | 4838a3a3c25cc9f7583dd62e4585460aca8ee961 (patch) | |
| tree | 80a909def685c23e426d350d494bdc1f00165459 /test-suite/bugs | |
| parent | 1cd87577ab85a402fb0482678dfcdbe85b45ce38 (diff) | |
Forcing i > Set for global universes (incomplete)
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/3309.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v index 980431576..6e97ed2af 100644 --- a/test-suite/bugs/closed/3309.v +++ b/test-suite/bugs/closed/3309.v @@ -117,7 +117,7 @@ intros. hnf. apply dirprodpair. exact ax0. apply dirprodpair. exact ax1. exact a Defined. Definition eqax0 { X : UU } { R : hrel X } { A : hsubtypes X } : iseqclass R A -> ishinh ( carrier A ) . -intros X R A; exact ( fun is : iseqclass R A => projT1' _ is ). +intros X R A. exact (fun is : iseqclass R A => projT1' _ is ). Defined. Lemma iseqclassdirprod { X Y : UU } { R : hrel X } { Q : hrel Y } { A : hsubtypes X } { B : hsubtypes Y } ( isa : iseqclass R A ) ( isb : iseqclass Q B ) : iseqclass ( hreldirprod R Q ) ( subtypesdirprod A B ) . @@ -141,7 +141,7 @@ Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f. admit. Defined. -Definition setquot { X : UU } ( R : hrel X ) : Type. +Definition setquot { X : UU } ( R : hrel X ) : Set. intros; exact ( sigT' ( fun A : _ => iseqclass R A ) ). Defined. Definition setquotpair { X : UU } ( R : hrel X ) ( A : hsubtypes X ) ( is : iseqclass R A ) : setquot R. @@ -157,7 +157,7 @@ Definition setquotinset { X : UU } ( R : hrel X ) : hSet. intros; exact ( hSetpair (setquot R) admit) . Defined. -Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ). +Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot@{i j k l m n p Set q r} RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ). intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2' _ ( projT1' _ cd ) ) ( projT2' _ ( projT2' _ cd ) ) ) ). Defined. |