replace (S 0) by 1, etc.; fix Makefile so TAGS file is in correct order

Main_Library/Generalities/uu1uu0.v

@@ -74,11 +74,11 @@ assert (s: uu1.isofhlevel n (paths _ x x')). apply (IHn _ (X0 x x')). apply (uu1
 
 Coercion u0isofhleveltou1isofhlevel: isofhlevel >-> uu1.isofhlevel.
 
-Definition u0isaproptou1isaprop (X : UU0) := u0isofhleveltou1isofhlevel (S O) X : isaprop X -> uu1.isaprop X.
+Definition u0isaproptou1isaprop (X : UU0) := u0isofhleveltou1isofhlevel 1 X : isaprop X -> uu1.isaprop X.
 Coercion u0isaproptou1isaprop : isaprop >-> uu1.isaprop.
 
 
-Definition u1isaproptou0isaprop (X : UU0) := u1isofhleveltou0isofhlevel (S O) X : uu1.isaprop X -> isaprop X.
+Definition u1isaproptou0isaprop (X : UU0) := u1isofhleveltou0isofhlevel 1 X : uu1.isaprop X -> isaprop X.
 Coercion u1isaproptou0isaprop : uu1.isaprop >-> isaprop.
 
 

Main_Library/hlevel1/hProp.v

@@ -88,7 +88,7 @@ Definition hfalse : hProp := hProppair empty isapropempty.
 Canonical Structure hfalse.
 
 
-Definition hconj (P Q : hProp) : hProp := hProppair (dirprod P Q) (isofhleveldirprod (S O) _ _ (uu1.pr22 _ _ P) (uu1.pr22 _ _ Q)). 
+Definition hconj (P Q : hProp) : hProp := hProppair (dirprod P Q) (isofhleveldirprod 1 _ _ (uu1.pr22 _ _ P) (uu1.pr22 _ _ Q)). 
 Canonical Structure hconj.
 
 Definition uu1hdisj (P Q : hProp) :=  ishinh (coprod P Q). 

Main_Library/hlevel1/hProp_up.v

@@ -54,7 +54,7 @@ set (is2:= uu1.gradth _ _ _ _ egf efg).
 apply ( uu1.isweqtotaltofib _ P1 P2  (fun XY: uu1.dirprod hProp hProp => (match XY with  uu1.tpair X Y => eqweqmaphProp X Y end)) is2 ( uu1.dirprodpair _ _ P P')). Defined. 
 
 Corollary uu1isasethProp : uu1.isaset hProp.
-Proof. unfold isaset.  simpl. intro. intro. apply (uu1.isofhlevelweqb (S O) _ _ _ (univfromtwoaxiomshProp x x') (uu1.isapropweq x x' (uu1.pr22 _ _ x'))). Defined.
+Proof. unfold isaset.  simpl. intro. intro. apply (uu1.isofhlevelweqb 1 _ _ _ (univfromtwoaxiomshProp x x') (uu1.isapropweq x x' (uu1.pr22 _ _ x'))). Defined.
 
 
 

Main_Library/hlevel2/finite_sets.v

@@ -120,14 +120,14 @@ Proof. intros X X0. apply (hinhpr _ (weqinv _ _ (weqpair _ _ _ (isweqtoempty _ X
 Corollary isof0elempty: isofnel O empty.
 Proof. apply (isof0elb empty (fun x:_ => x)). Defined. 
 
-Lemma isof1ela (X:UU0): isofnel (S O) X -> iscontr X.
-Proof. intros X X0.  apply (isofnelimpl (S O) X X0 (iscontr_hprop X)).  set (w2:= (weqinv _ _ (weqfromcoprodwithempty unit))). intro X1.  set (w3:= weqcomp _ _ _ w2 X1). apply (iscontrifweqtounit _ (weqinv _ _ w3)). assumption. Defined.  
+Lemma isof1ela (X:UU0): isofnel 1 X -> iscontr X.
+Proof. intros X X0.  apply (isofnelimpl 1 X X0 (iscontr_hprop X)).  set (w2:= (weqinv _ _ (weqfromcoprodwithempty unit))). intro X1.  set (w3:= weqcomp _ _ _ w2 X1). apply (iscontrifweqtounit _ (weqinv _ _ w3)). assumption. Defined.  
 
-Lemma isof1elb (X:UU0): (iscontr X) -> isofnel (S O) X.
+Lemma isof1elb (X:UU0): (iscontr X) -> isofnel 1 X.
 Proof. intros X X0. set (w1:= weqpair _ _ _ (isweqcontrtounit _ X0)). set (w2:= weqfromcoprodwithempty unit).  set (w:= weqcomp _ _ _ w2 (weqinv _ _ w1)). apply (hinhpr _ w). Defined. 
 
 
-Lemma isof1elunit: isofnel (S O) unit.
+Lemma isof1elunit: isofnel 1 unit.
 Proof. apply (hinhpr _ (weqfromcoprodwithempty unit)). Defined. 
 
 
@@ -140,8 +140,8 @@ Lemma isofnelweqf (n:nat)(X Y:UU0)(f:X -> Y)(is: isweq _ _ f): isofnel n X -> is
 Proof. intros n X Y f is X0.  set (ff:= fun u:weq (stn n) X => weqcomp _ _ _ u (weqpair _ _ f is)). apply (hinhfunct _ _ ff X0). Defined.
 
 
-Lemma isof2elbool : isofnel (S (S O)) bool.
-Proof. apply (isofnelweqf _ _ _ _ (pr22 _ _ boolascoprod) (isofsnel (S O) unit isof1elunit)). Defined. 
+Lemma isof2elbool : isofnel 2 bool.
+Proof. apply (isofnelweqf _ _ _ _ (pr22 _ _ boolascoprod) (isofsnel 1 unit isof1elunit)). Defined. 
 
 
 
@@ -214,7 +214,7 @@ Defined.
 
 Definition weqtoinitintervalsn  (n:nat) : weq  (coprod (initinterval n) unit) (initinterval (S n)).
 Proof. intro. set (f:= toinitintervalsn n). set (g:= frominitintervalsn n). split with f. 
-set (u:= coprodf _ _ _ _ (initintervaltonat n) (fun t:unit => t)).   assert (is: isincl _ _ u). apply (isofhlevelfcoprodf (S O) _ _ _ _ _ _ (isinclinitintervaltonat n) (isofhlevelfweq (S O) _ _ _ (idisweq unit))).  
+set (u:= coprodf _ _ _ _ (initintervaltonat n) (fun t:unit => t)).   assert (is: isincl _ _ u). apply (isofhlevelfcoprodf 1 _ _ _ _ _ _ (isinclinitintervaltonat n) (isofhlevelfweq 1 _ _ _ (idisweq unit))).  
 assert (egf: forall x:_, paths _ (g (f x)) x).  intro. 
 assert (egf0: paths _ (u (g (f x))) (u x)).  destruct x. simpl. destruct i as [ t x ]. destruct t.   simpl.  apply idpath. simpl. destruct (isdeceqnat n t).    simpl. induction p. apply (initmap _ (neglebsnn t x)).  simpl.  apply idpath.  destruct u0. destruct n.  apply idpath. simpl.  destruct (isdeceqnat n n) as [|e]. apply idpath.  apply (initmap _ (e (idpath _ _))). apply (invmaponpathsincl _ _ _ is _ _ egf0). 
 assert (efg: forall x:_, paths _ (f (g x)) x). intro. 
@@ -264,7 +264,7 @@ Proof.
     assert (c1: decidable (paths _ t t0)).
     apply isdeceqnat.
     destruct c1.
-      apply (invmaponpathsincl (isfinite0 X) nat (pr21 _ _) (isofhlevelfpr21 (S O) _ _  (fun n:nat => isapropdneg (weq (stn n) X))) (tpair nat (fun n : nat => isofnel0 n X) t x0) (tpair nat (fun n : nat => isofnel0 n X) t0 x) p).
+      apply (invmaponpathsincl (isfinite0 X) nat (pr21 _ _) (isofhlevelfpr21 1 _ _  (fun n:nat => isapropdneg (weq (stn n) X))) (tpair nat (fun n : nat => isofnel0 n X) t x0) (tpair nat (fun n : nat => isofnel0 n X) t0 x) p).
     assert (is1: dneg (dirprod (weq (stn t0) X) (weq (stn t) X))).
       apply (dneganddnegimpldneg _ _ x x0).
     assert (is2: dneg (weq (stn t0) (stn t))).
@@ -302,10 +302,10 @@ Definition isfinitestn (n:nat): isfinite (stn n) := hinhpr _ (finitestructstn n)
 Definition finitestructempty := finitestructpair _ O (idweq _).
 Definition isfiniteempty : isfinite empty := hinhpr _ finitestructempty.
 
-Definition finitestructunit: finitestruct unit := finitestructpair _ (S O) (weqfromcoprodwithempty unit).
+Definition finitestructunit: finitestruct unit := finitestructpair _ 1 (weqfromcoprodwithempty unit).
 Definition isfiniteunit : isfinite unit := hinhpr _ finitestructunit. 
 
-Definition finitestructbool := finitestructpair _ (S (S O)) (weqcomp _ _ _ (weqcoprodf _ _ _ _ (weqfromcoprodwithempty unit) (idweq unit)) boolascoprod).
+Definition finitestructbool := finitestructpair _ 2 (weqcomp _ _ _ (weqcoprodf _ _ _ _ (weqfromcoprodwithempty unit) (idweq unit)) boolascoprod).
 Definition isfinitebool : isfinite bool  := hinhpr _ finitestructbool.
 
 Definition finitestructinitinterval (n:nat) := finitestructpair _ (S n) (weqstntoinitinterval n).
@@ -434,7 +434,7 @@ Proof. intros. *)
 
 
 
-(*Eval compute in carddneg _  (isfinitedirprod _ _ (isfinitestn (S (S (S (S O)))))  (isfinitestn (S (S (S O))))).*)
+(*Eval compute in carddneg _  (isfinitedirprod _ _ (isfinitestn 4)  (isfinitestn 3)).*)
 
 Eval compute in carddneg _ (isfiniteempty).
 
@@ -456,7 +456,7 @@ Eval compute in carddneg _ (isfinitedirprod _ _ isfinitebool isfinitebool).
 
 Eval compute in carddneg _ (isfinitedirprod _ _ isfinitebool (isfinitedirprod _ _ isfinitebool isfinitebool)).
 
-Eval compute in carddneg _ (isfinitecoprod _ _ (isfinitebool) (isfinitecomplement _ (ii1 _ _ (ii2 _ _ tt)) (isfinitestn (S (S (S O)))))).
+Eval compute in carddneg _ (isfinitecoprod _ _ (isfinitebool) (isfinitecomplement _ (ii1 _ _ (ii2 _ _ tt)) (isfinitestn 3))).
 
 Eval lazy in carddneg _ (isfinitecomplement _ (ii1 _ _ tt) (isfinitecoprod _ _ (isfiniteunit) (isfinitebool))).
 
@@ -465,7 +465,7 @@ Eval lazy in carddneg _ (isfinitecomplement _ (ii1 _ _ tt) (isfinitecoprod _ _ (
 (*Eval compute in carddneg _ (isfinitecomplement _ (dirprodpair _ _ tt tt) (isfinitedirprod _ _ isfiniteunit isfiniteunit)).*)
 
 
-(*Definition finitestructunit: finitestruct unit := finitestructpair _ (S O) (weqfromcoprodwithempty unit).*)
+(*Definition finitestructunit: finitestruct unit := finitestructpair _ 1 (weqfromcoprodwithempty unit).*)
 
 Eval lazy in (pr21 _ _ (finitestructcomplement _ (dirprodpair _ _ tt tt) (finitestructdirprod _ _ (finitestructunit) (finitestructunit)))).
 
@@ -483,16 +483,16 @@ Eval lazy in carddneg _ (isfinitecomplement _ (dirprodpair _ _ true (dirprodpair
 
 (*
 
-Eval compute in (pr21 _ _ (isfinitedirprod _ _ (isfinitestn (S (S (S (S O)))))  (isfinitestn (S (S (S O)))))).
+Eval compute in (pr21 _ _ (isfinitedirprod _ _ (isfinitestn 4)  (isfinitestn 3))).
 
 
 Print empty_rect. 
 
-Lemma isof1elfrom0el (X Y:UU0): isofnel O X -> isofnel (S O) (X -> Y).
+Lemma isof1elfrom0el (X Y:UU0): isofnel O X -> isofnel 1 (X -> Y).
 Proof. intros. unfold isofnel. intro.   simpl. 
 
 Theorem isfinitefunctions (X Y:UU0)(isx: isfinite X)(isy: isfinite Y): isfinite (X -> Y).
-Proof. intros. destruct isx.  generalize Y isy X x. clear isy Y x X.  induction t.  intros. split with (S O). 
+Proof. intros. destruct isx.  generalize Y isy X x. clear isy Y x X.  induction t.  intros. split with 1. 
 
 
 

Main_Library/hlevel2/set_quotients_r_up.v

@@ -102,7 +102,7 @@ set (r1:= pr21 _ _ (pr22 _ _ is)). unfold issymm in r1.
 set (ax := is1 x x' a). set (ax' := is1 x' x (r1 _ _ a)). 
 set (f:= fun u: R x t => (r1 _ _ (ax (r1 _ _ u)))). set (g:= fun u: R x' t => (r1 _ _ (ax' (r1 _ _ u)))). 
 apply (uahp _ _ f g). 
-set (is2:= isofhlevelfpr21 (S O) _ _ (fun A: hsubtypes X =>  (isapropiseqclass X R A))).  
+set (is2:= isofhlevelfpr21 1 _ _ (fun A: hsubtypes X =>  (isapropiseqclass X R A))).  
 apply (invmaponpathsincl _ _ _ is2 _ _ e). Defined. (* Uses univalence for hProp *)
 
 

Makefile

@@ -2,20 +2,20 @@
 M=Main_Library
 P=Proof_of_Extensionality
 COQFLAGS = -opt -q
-VFILES :=								\
-	$M/Generalities/uu0.v						\
-	$M/Generalities/uu1.v						\
-	$M/Generalities/uu1uu0.v					\
-	$P/univ01.v							\
-	$M/hlevel1/hProp.v						\
-	$M/hlevel2/finite_sets.v					\
-	$M/hlevel1/hProp_up.v						\
-	$M/hlevel1/hProp_r.v						\
-	$M/hlevel1/hProp_r_up.v						\
-	$M/hlevel2/hSet_r.v						\
-	$M/hlevel2/hSet_r_up.v						\
-	$M/hlevel2/set_quotients_r_up.v					\
-	$M/hlevel2/set_quotients_constr2_r_up.v 		
+VFILES :=					\
+	$M/hlevel2/set_quotients_constr2_r_up.v	\
+	$M/hlevel2/set_quotients_r_up.v		\
+	$M/hlevel2/hSet_r_up.v			\
+	$M/hlevel2/hSet_r.v			\
+	$M/hlevel1/hProp_r_up.v			\
+	$M/hlevel1/hProp_r.v			\
+	$M/hlevel1/hProp_up.v			\
+	$M/hlevel2/finite_sets.v		\
+	$M/hlevel1/hProp.v			\
+	$P/univ01.v				\
+	$M/Generalities/uu1uu0.v		\
+	$M/Generalities/uu1.v			\
+	$M/Generalities/uu0.v
 VOFILES := $(VFILES:.v=.vo)
 MADE_FILES = 
 %.glob %.vo: %.v
@@ -46,6 +46,7 @@ $M/Generalities/uu1.v: $M/Generalities/uu0.v Makefile uu1.sed
 	rm -f $@
 	sed <$< >$@ -f uu1.sed
 	chmod a-w $@
+$M/Generalities/uu1.vo:| $M/Generalities/uu0.vo
 
 $P/univ01.vo $M/Generalities/uu1uu0.vo: $M/Generalities/uu0.vo $M/Generalities/uu1.vo
 clean: