Semi-final version for MSCS

Author: vladimirias

Generalities/uu0.v

@@ -1867,7 +1867,7 @@ Proof. intros. apply isofhleveltotal2. assumption. intro. assumption. Defined.
 (** *** Basics about types of h-level 1 - "propositions" *)
 
 
-Definition isaprop  := isofhlevel (S O)  . 
+Definition isaprop  := isofhlevel (S O) . 
 
 Notation isapropunit := iscontrpathsinunit .
 
@@ -1940,18 +1940,12 @@ Theorem isapropempty: isaprop empty.
 Proof. unfold isaprop. unfold isofhlevel. intros x x' . destruct x. Defined. 
 
 
-Theorem isapropempty2 { X : UU } ( a : X -> empty ) : isaprop X .
+Theorem isapropifnegtrue { X : UU } ( a : X -> empty ) : isaprop X .
 Proof . intros . set ( w := weqpair _ ( isweqtoempty a ) ) . apply ( isofhlevelweqb 1 w isapropempty ) .  Defined .
 
 
 
 
-Lemma isapropifnegtrue { X : UU } ( X0 : neg X ) : isaprop X.
-Proof. intros X X0. assert (is:isweq X0). intro. apply (fromempty y).   apply (isofhlevelweqb (S O)  ( weqpair _ is ) isapropempty). Defined. 
-
-
-
-
 (** *** Functional extensionality for functions to the empty type *)
 
 Axiom funextempty : forall ( X : UU ) ( f g : X -> empty ) , paths f g . 
@@ -2084,7 +2078,9 @@ apply ( isapropifcontr is4  ). Defined.
 
 (** *** Basics about types of h-level 2 - "sets" *)
 
-Definition isaset ( X : UU ) : UU := forall x x' : X , isaprop ( paths x x' ) . 
+Definition isaset ( X : UU ) : UU := forall x x' : X , isaprop ( paths x x' ) .
+
+(* Definition isaset := isofhlevel 2 . *)
 
 Notation isasetdirprod := ( isofhleveldirprod 2 ) .
 
@@ -2943,6 +2939,7 @@ Definition sectohfibertosec { X : UU } (P:X -> UU): forall a: forall x:X, P x, p
 
 Axiom funextfunax : forall (X Y:UU)(f g:X->Y),  (forall x:X, paths (f x) (g x)) -> (paths f g). 
 
+
 Lemma isweqlcompwithweq { X X' : UU} (w: weq X X') (Y:UU) : isweq (fun a:X'->Y => (fun x:X => a (w x))).
 Proof. intros. set (f:= (fun a:X'->Y => (fun x:X => a (w x)))). set (g := fun b:X-> Y => fun x':X' => b ( invweq  w x')). 
 set (egf:= (fun a:X'->Y => funextfunax X' Y (fun x':X' => (g (f a)) x') a (fun x': X' =>  maponpaths a  (homotweqinvweq w x')))).
@@ -3163,7 +3160,7 @@ Definition weqforalltohfiber  { X : UU } (P Q : X -> UU) (f: forall x:X, P x ->
 
 
 
-(** *** The weqk equivalence  between section spaces (dependent products) defined by a family of weak equivalences  [ weq ( P x ) ( Q x ) ] *)
+(** *** The weak equivalence  between section spaces (dependent products) defined by a family of weak equivalences  [ weq ( P x ) ( Q x ) ] *)
 
 
 
@@ -3434,7 +3431,7 @@ Proof. intros. apply impred. intro.   assumption.  Defined.
 
 
 Theorem isapropneg2 ( X : UU ) { Y : UU } ( is : neg Y ) : isaprop ( X -> Y ) .
-Proof . intros .  apply impred . intro . apply ( isapropempty2 is ) . Defined .   
+Proof . intros .  apply impred . intro . apply ( isapropifnegtrue  is ) . Defined .   
 
 
 
@@ -3609,7 +3606,7 @@ Proof . intro . apply ( isofhlevelsnweqtohlevelsn 0 _ _ ( isapropempty ) ) . Def
 
 
 Theorem isapropweqtoempty2 ( X : UU ) { Y : UU } ( is : neg Y ) : isaprop ( weq X Y ) .
-Proof. intros . apply ( isofhlevelsnweqtohlevelsn 0 _ _ ( isapropempty2 is ) ) . Defined . 
+Proof. intros . apply ( isofhlevelsnweqtohlevelsn 0 _ _ ( isapropifnegtrue is ) ) . Defined . 
 
 
 (** *** Weak equivalences from an empty type *)
@@ -3618,7 +3615,7 @@ Theorem isapropweqfromempty ( X : UU ) : isaprop ( weq empty X ) .
 Proof . intro . apply ( isofhlevelsnweqfromhlevelsn 0 X _ ( isapropempty ) ) . Defined . 
 
 Theorem isapropweqfromempty2 ( X : UU ) { Y : UU } ( is : neg Y ) : isaprop ( weq Y X ) .
-Proof. intros .  apply ( isofhlevelsnweqfromhlevelsn 0 X _ ( isapropempty2 is ) ) .  Defined .
+Proof. intros .  apply ( isofhlevelsnweqfromhlevelsn 0 X _ ( isapropifnegtrue is ) ) .  Defined .
 
 
 

hlevel1/hProp.v

@@ -28,19 +28,19 @@ Require Export Foundations.hlevel2.hSet .
 
 (** **** General definitions *)
 
-Definition binop ( X : UU0 ) := X -> X -> X .
+Definition binop ( X : UU ) := X -> X -> X .
 
-Definition islcancelable { X : UU0 } ( opp : binop X ) ( x : X ) := isincl ( fun x0 : X => opp x x0 ) .
+Definition islcancelable { X : UU } ( opp : binop X ) ( x : X ) := isincl ( fun x0 : X => opp x x0 ) .
 
-Definition isrcancelable { X : UU0 } ( opp : binop X ) ( x : X ) := isincl ( fun x0 : X => opp x0 x ) .
+Definition isrcancelable { X : UU } ( opp : binop X ) ( x : X ) := isincl ( fun x0 : X => opp x0 x ) .
 
-Definition iscancelable { X : UU0 } ( opp : binop X ) ( x : X )  := dirprod ( islcancelable opp x ) ( isrcancelable opp x ) . 
+Definition iscancelable { X : UU } ( opp : binop X ) ( x : X )  := dirprod ( islcancelable opp x ) ( isrcancelable opp x ) . 
 
-Definition islinvertible { X : UU0 } ( opp : binop X ) ( x : X ) := isweq ( fun x0 : X => opp x x0 ) .
+Definition islinvertible { X : UU } ( opp : binop X ) ( x : X ) := isweq ( fun x0 : X => opp x x0 ) .
 
-Definition isrinvertible { X : UU0 } ( opp : binop X ) ( x : X ) := isweq ( fun x0 : X => opp x0 x ) .
+Definition isrinvertible { X : UU } ( opp : binop X ) ( x : X ) := isweq ( fun x0 : X => opp x0 x ) .
 
-Definition isinvertible { X : UU0 } ( opp : binop X ) ( x : X ) := dirprod ( islinvertible opp x ) ( isrinvertible opp x ) . 
+Definition isinvertible { X : UU } ( opp : binop X ) ( x : X ) := dirprod ( islinvertible opp x ) ( isrinvertible opp x ) . 
 
 
 
@@ -422,7 +422,7 @@ Definition isbinopfun { X Y : setwithbinop } ( f : X -> Y ) := forall x x' : X ,
 Lemma isapropisbinopfun { X Y : setwithbinop } ( f : X -> Y ) : isaprop ( isbinopfun f ) .
 Proof . intros . apply impred . intro x . apply impred . intro x' . apply ( setproperty Y ) . Defined .
 
-Definition binopfun ( X Y : setwithbinop ) : UU0 := total2 ( fun f : X -> Y => isbinopfun f ) .
+Definition binopfun ( X Y : setwithbinop ) : UU := total2 ( fun f : X -> Y => isbinopfun f ) .
 Definition binopfunpair { X Y : setwithbinop } ( f : X -> Y ) ( is : isbinopfun f ) : binopfun X Y := tpair _ f is . 
 Definition pr1binopfun ( X Y : setwithbinop ) : binopfun X Y -> ( X -> Y ) := @pr1 _ _ . 
 Coercion pr1binopfun : binopfun >-> Funclass . 
@@ -438,7 +438,7 @@ Opaque isbinopfuncomp .
 Definition binopfuncomp { X Y Z : setwithbinop } ( f : binopfun X Y ) ( g : binopfun Y Z ) : binopfun X Z := binopfunpair ( funcomp ( pr1 f ) ( pr1 g ) ) ( isbinopfuncomp f g ) . 
 
 
-Definition binopmono ( X Y : setwithbinop ) : UU0 := total2 ( fun f : incl X Y => isbinopfun ( pr1 f ) ) .
+Definition binopmono ( X Y : setwithbinop ) : UU := total2 ( fun f : incl X Y => isbinopfun ( pr1 f ) ) .
 Definition binopmonopair { X Y : setwithbinop } ( f : incl X Y ) ( is : isbinopfun f ) : binopmono X Y := tpair _  f is .
 Definition pr1binopmono ( X Y : setwithbinop ) : binopmono X Y -> incl X Y := @pr1 _ _ .
 Coercion pr1binopmono : binopmono >-> incl .
@@ -449,7 +449,7 @@ Coercion binopincltobinopfun : binopmono >-> binopfun .
 
 Definition binopmonocomp { X Y Z : setwithbinop } ( f : binopmono X Y ) ( g : binopmono Y Z ) : binopmono X Z := binopmonopair ( inclcomp ( pr1 f ) ( pr1 g ) ) ( isbinopfuncomp f g ) . 
 
-Definition binopiso ( X Y : setwithbinop ) : UU0 := total2 ( fun f : weq X Y => isbinopfun f ) .   
+Definition binopiso ( X Y : setwithbinop ) : UU := total2 ( fun f : weq X Y => isbinopfun f ) .   
 Definition binopisopair { X Y : setwithbinop } ( f : weq X Y ) ( is : isbinopfun f ) : binopiso X Y := tpair _  f is .
 Definition pr1binopiso ( X Y : setwithbinop ) : binopiso X Y -> weq X Y := @pr1 _ _ .
 Coercion pr1binopiso : binopiso >-> weq .
@@ -804,7 +804,7 @@ Definition istwobinopfun { X Y : setwith2binop } ( f : X -> Y ) := dirprod ( for
 Lemma isapropistwobinopfun { X Y : setwith2binop } ( f : X -> Y ) : isaprop ( istwobinopfun f ) .
 Proof . intros . apply isofhleveldirprod . apply impred . intro x . apply impred . intro x' . apply ( setproperty Y ) . apply impred . intro x . apply impred . intro x' . apply ( setproperty Y ) . Defined .
 
-Definition twobinopfun ( X Y : setwith2binop ) : UU0 := total2 ( fun f : X -> Y => istwobinopfun f ) .
+Definition twobinopfun ( X Y : setwith2binop ) : UU := total2 ( fun f : X -> Y => istwobinopfun f ) .
 Definition twobinopfunpair { X Y : setwith2binop } ( f : X -> Y ) ( is : istwobinopfun f ) : twobinopfun X Y := tpair _ f is . 
 Definition pr1twobinopfun ( X Y : setwith2binop ) : twobinopfun X Y -> ( X -> Y ) := @pr1 _ _ . 
 Coercion pr1twobinopfun : twobinopfun >-> Funclass .
@@ -827,7 +827,7 @@ Opaque istwobinopfuncomp .
 Definition twobinopfuncomp { X Y Z : setwith2binop } ( f : twobinopfun X Y ) ( g : twobinopfun Y Z ) : twobinopfun X Z := twobinopfunpair ( funcomp ( pr1 f ) ( pr1 g ) ) ( istwobinopfuncomp f g ) . 
 
 
-Definition twobinopmono ( X Y : setwith2binop ) : UU0 := total2 ( fun f : incl X Y => istwobinopfun f ) .
+Definition twobinopmono ( X Y : setwith2binop ) : UU := total2 ( fun f : incl X Y => istwobinopfun f ) .
 Definition twobinopmonopair { X Y : setwith2binop } ( f : incl X Y ) ( is : istwobinopfun f ) : twobinopmono X Y := tpair _  f is .
 Definition pr1twobinopmono ( X Y : setwith2binop ) : twobinopmono X Y -> incl X Y := @pr1 _ _ .
 Coercion pr1twobinopmono : twobinopmono >-> incl .
@@ -841,7 +841,7 @@ Definition binop2mono { X Y : setwith2binop } ( f : twobinopmono X Y ) : binopmo
 
 Definition twobinopmonocomp { X Y Z : setwith2binop } ( f : twobinopmono X Y ) ( g : twobinopmono Y Z ) : twobinopmono X Z := twobinopmonopair ( inclcomp ( pr1 f ) ( pr1 g ) ) ( istwobinopfuncomp f g ) . 
 
-Definition twobinopiso ( X Y : setwith2binop ) : UU0 := total2 ( fun f : weq X Y => istwobinopfun f ) .   
+Definition twobinopiso ( X Y : setwith2binop ) : UU := total2 ( fun f : weq X Y => istwobinopfun f ) .   
 Definition twobinopisopair { X Y : setwith2binop } ( f : weq X Y ) ( is : istwobinopfun f ) : twobinopiso X Y := tpair _  f is .
 Definition pr1twobinopiso ( X Y : setwith2binop ) : twobinopiso X Y -> weq X Y := @pr1 _ _ .
 Coercion pr1twobinopiso : twobinopiso >-> weq .

hlevel2/algebra1a.v

@@ -62,7 +62,7 @@ Definition ismonoidfun { X Y : monoid } ( f : X -> Y ) := dirprod ( isbinopfun f
 Lemma isapropismonoidfun { X Y : monoid } ( f : X -> Y ) : isaprop ( ismonoidfun f ) .
 Proof . intros . apply isofhleveldirprod . apply isapropisbinopfun .  apply ( setproperty Y ) . Defined .
 
-Definition monoidfun ( X Y : monoid ) : UU0 := total2 ( fun f : X -> Y => ismonoidfun f ) .
+Definition monoidfun ( X Y : monoid ) : UU := total2 ( fun f : X -> Y => ismonoidfun f ) .
 Definition monoidfunconstr { X Y : monoid } { f : X -> Y } ( is : ismonoidfun f ) : monoidfun X Y := tpair _ f is . 
 Definition pr1monoidfun ( X Y : monoid ) : monoidfun X Y -> ( X -> Y ) := @pr1 _ _ . 
 
@@ -82,7 +82,7 @@ Opaque ismonoidfuncomp .
 Definition monoidfuncomp { X Y Z : monoid } ( f : monoidfun X Y ) ( g : monoidfun Y Z ) : monoidfun X Z := monoidfunconstr ( ismonoidfuncomp f g ) . 
 
 
-Definition monoidmono ( X Y : monoid ) : UU0 := total2 ( fun f : incl X Y => ismonoidfun f ) .
+Definition monoidmono ( X Y : monoid ) : UU := total2 ( fun f : incl X Y => ismonoidfun f ) .
 Definition monoidmonopair { X Y : monoid } ( f : incl X Y ) ( is : ismonoidfun f ) : monoidmono X Y := tpair _  f is .
 Definition pr1monoidmono ( X Y : monoid ) : monoidmono X Y -> incl X Y := @pr1 _ _ .
 Coercion pr1monoidmono : monoidmono >-> incl .
@@ -96,7 +96,7 @@ Coercion monoidmonotobinopmono : monoidmono >-> binopmono .
 Definition monoidmonocomp { X Y Z : monoid } ( f : monoidmono X Y ) ( g : monoidmono Y Z ) : monoidmono X Z := monoidmonopair ( inclcomp ( pr1 f ) ( pr1 g ) ) ( ismonoidfuncomp f g ) . 
 
 
-Definition monoidiso ( X Y : monoid ) : UU0 := total2 ( fun f : weq X Y => ismonoidfun f ) .   
+Definition monoidiso ( X Y : monoid ) : UU := total2 ( fun f : weq X Y => ismonoidfun f ) .   
 Definition monoidisopair { X Y : monoid } ( f : weq X Y ) ( is : ismonoidfun f ) : monoidiso X Y := tpair _  f is .
 Definition pr1monoidiso ( X Y : monoid ) : monoidiso X Y -> weq X Y := @pr1 _ _ .
 Coercion pr1monoidiso : monoidiso >-> weq .

hlevel2/algebra1b.v

@@ -22,7 +22,7 @@ Require Export Foundations.hlevel2.algebra1c .
 
 (** To hSet *)
 
-Lemma rtoneq { X : UU0 } { R : hrel X } ( is : isirrefl R ) { a b : X } ( r : R a b ) : neg ( paths a b ) .
+Lemma rtoneq { X : UU } { R : hrel X } ( is : isirrefl R ) { a b : X } ( r : R a b ) : neg ( paths a b ) .
 Proof . intros . intro e . rewrite e in r . apply ( is b r ) . Defined .  
 
 (** To one binary operation *)