Reduce universe variables and other clean-ups

theories/Algebra/AbGroups/Z.v

@@ -8,7 +8,11 @@ Require Import Algebra.AbGroups.AbelianGroup.
 
 Local Open Scope int_scope.
 
-Definition abgroup_Z : AbGroup.
+Section MinimizationToSet.
+
+Local Set Universe Minimization ToSet.
+
+Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
   snrapply Build_AbGroup.
   - refine (Build_Group Int int_add 0 int_negation _); repeat split.
@@ -20,6 +24,8 @@ Proof.
   - exact int_add_comm.
 Defined.
 
+End MinimizationToSet.
+
 (** We can multiply by [n : Int] in any abelian group. *)
 Definition ab_mul (n : Int) {A : AbGroup} : GroupHomomorphism A A.
 Proof.

theories/Algebra/Groups/Group.v

@@ -251,6 +251,7 @@ Definition pequiv_groupisomorphism {A B : Group}
   := fun f => Build_pEquiv _ _ f _.
 
 Coercion equiv_groupisomorphism : GroupIsomorphism >-> Equiv.
+Coercion pequiv_groupisomorphism : GroupIsomorphism >-> pEquiv.
 
 Definition equiv_path_groupisomorphism `{F : Funext} {G H : Group}
   (f g : GroupIsomorphism G H)

theories/Homotopy/SuccessorStructure.v

@@ -1,8 +1,11 @@
 Require Import Basics.
+Require Import Nat.Core.
 Require Import Spaces.Int.
 Require Import Spaces.Finite.Fin.
 Require Import WildCat.
 
+Local Set Universe Minimization ToSet.
+
 (** * Successor Structures. *)
 
 (** A successor structure is just a type with a endofunctor on it, called 'successor'. Typical examples include either the integers or natural numbers with the successor (or predecessor) operation. *)
@@ -15,6 +18,7 @@ Record SuccStr : Type := {
 Declare Scope succ_scope.
 
 Local Open Scope nat_scope.
+Local Open Scope type_scope.
 Local Open Scope succ_scope.
 
 Delimit Scope succ_scope with succ.
@@ -33,14 +37,16 @@ Notation "'+Z'" := IntSucc : succ_scope.
 
 (** Stratified successor structures *)
 
-Definition StratifiedType (N : SuccStr) (n : nat) : Type := N * Fin n.
+(** If [N] has a successor structure, then so does the product [N * Fin n].  The successor operation increases the second factor, and if it wraps around, it also increases the first factor. *)
+
+Definition StratifiedType (N : SuccStr) (n : nat) := N * Fin n.
 
 Definition stratified_succ (N : SuccStr) (n : nat) (x : StratifiedType N n)
   : StratifiedType N n.
 Proof.
   constructor.
-  + induction n.
-    - induction (snd x).
+  + destruct n.
+    - exact (Empty_rec _ (snd x)).
     - destruct (dec (snd x = inr tt)).
       * exact (ss_succ (fst x)).
       * exact (fst x).
@@ -51,21 +57,17 @@ Definition Stratified (N : SuccStr) (n : nat) : SuccStr
   := Build_SuccStr (StratifiedType N n) (stratified_succ N n).
 
 (** Addition in successor structures *)
-Fixpoint ss_add {N : SuccStr} (n : N) (k : nat) : N :=
-  match k with
-  | O   => n
-  | S k => (ss_add n k).+1
-  end.
+Definition ss_add {N : SuccStr} (n : N) (k : nat) : N := nat_iter k ss_succ n.
 
 Infix "+" := ss_add : succ_scope.
 
 Definition ss_add_succ {N : SuccStr} (n : N) (k : nat)
-  : (n + k.+1) = n.+1 + k.
-Proof.
-  induction k.
-  + reflexivity.
-  + exact (ap ss_succ IHk).
-Defined.
+  : n + k.+1 = n.+1 + k
+  := nat_iter_succ_r k ss_succ n.
+
+Definition ss_add_sum {N : SuccStr} (n : N) (k l : nat)
+  : n + (k + l) = (n + l) + k
+  := nat_iter_add k l ss_succ n.
 
 (** Nat and Int segmented by triples *)
 Notation "'N3'" := (Stratified (+N) 3) : succ_scope.