diff --git a/test/Algebra/Rings/Matrix.v b/test/Algebra/Rings/Matrix.v
index 5c70cfbf768..88632a6dfab 100644
--- a/test/Algebra/Rings/Matrix.v
+++ b/test/Algebra/Rings/Matrix.v
@@ -1,7 +1,7 @@
 From HoTT Require Import Basics.
 From HoTT Require Import Algebra.Rings.Matrix.
 From HoTT Require Import Spaces.Nat.Core Spaces.List.Core.
-From HoTT Require Import Algebra.Rings.Z Spaces.BinInt.Core Algebra.Rings.CRing.
+From HoTT Require Import Algebra.Rings.Z Spaces.Int Algebra.Rings.CRing.
 From HoTT Require Import Classes.interfaces.canonical_names.
 
 Local Open Scope mc_scope.
@@ -38,7 +38,7 @@ Definition test2_B := Build_Matrix' nat 4 4
 
 Definition test2 : entries test2_A = entries test2_B := idpath.
 
-Local Open Scope binint_scope.
+Local Open Scope int_scope.
 
 (** Matrices with ring entries can be multiplied *)
 
diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index 272bffa5f7f..7c9a818bbed 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -228,6 +228,20 @@ Proof.
     1-2: exact negate_involutive.
 Defined.
 
+(** This goal comes up twice in the proof of [ab_mul], so we factor it out. *)
+Local Definition ab_mul_helper {A : AbGroup} (a b x y z : A)
+  (p : x = y + z)
+  : a + b + x = a + y + (b + z).
+Proof.
+  lhs_V srapply grp_assoc.
+  rhs_V srapply grp_assoc.
+  apply grp_cancelL.
+  rhs srapply grp_assoc.
+  rhs nrapply (ap (fun g => g + z) (ab_comm y b)).
+  rhs_V srapply grp_assoc.
+  apply grp_cancelL, p.
+Defined.
+
 (** Multiplication by [n : Int] defines an endomorphism of any abelian group [A]. *)
 Definition ab_mul {A : AbGroup} (n : Int) : GroupHomomorphism A A.
 Proof.
@@ -236,32 +250,18 @@ Proof.
   intros a b.
   induction n; cbn.
   - exact (grp_unit_l _)^.
-  - destruct n.
-    + reflexivity.
-    + rhs_V srapply (associativity a).
-      rhs srapply (ap _ (associativity _ b _)).
-      rewrite (commutativity (nat_iter _ _ _) b).
-      rhs_V srapply (ap _ (associativity b _ _)).
-      rhs srapply (associativity a).
-      apply grp_cancelL.
-      exact IHn.
-  - destruct n.
-    + rewrite (commutativity (-a)).
-      exact (grp_inv_op a b).
-    + rhs_V srapply (associativity (-a)).
-      rhs srapply (ap _ (associativity _ (-b) _)).
-      rewrite (commutativity (nat_iter _ _ _) (-b)).
-      rhs_V srapply (ap _ (associativity (-b) _ _)).
-      rhs srapply (associativity (-a)).
-      rewrite (commutativity (-a) (-b)), <- (grp_inv_op a b).
-      apply grp_cancelL.
-      exact IHn.
+  - rewrite 3 grp_pow_succ.
+    by apply ab_mul_helper.
+  - rewrite 3 grp_pow_pred.
+    rewrite (grp_inv_op a b), (commutativity (-b) (-a)).
+    by apply ab_mul_helper.
 Defined.
 
-Definition ab_mul_homo {A B : AbGroup}
+(** [ab_mul n] is natural. *)
+Definition ab_mul_natural {A B : AbGroup}
   (f : GroupHomomorphism A B) (n : Int)
   : f o ab_mul n == ab_mul n o f
-  := grp_pow_homo f n.
+  := grp_pow_natural f n.
 
 (** The image of an inclusion is a normal subgroup. *)
 Definition ab_image_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f} : NormalSubgroup B
@@ -303,18 +303,17 @@ Proof.
 Defined.
 
 (** If the function is constant in the range of a finite sum then the sum is equal to the constant times [n]. This is a group power in the underlying group. *)
-Definition ab_sum_const {A : AbGroup} (n : nat) (r : A)
-  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = r)
-  : ab_sum n f = grp_pow r n.
+Definition ab_sum_const {A : AbGroup} (n : nat) (a : A)
+  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = a)
+  : ab_sum n f = ab_mul n a.
 Proof.
   induction n as [|n IHn] in f, p |- *.
   - reflexivity.
   - rhs nrapply (ap@{Set _} _ (int_of_nat_succ_commute n)).
-    rhs nrapply grp_pow_int_add_1.
+    rhs nrapply grp_pow_succ.
     simpl. f_ap.
-    rewrite IHn.
-    + reflexivity.
-    + intros. apply p.
+    apply IHn.
+    intros. apply p.
 Defined.
 
 (** If the function is zero in the range of a finite sum then the sum is zero. *)
diff --git a/theories/Algebra/AbGroups/Cyclic.v b/theories/Algebra/AbGroups/Cyclic.v
index af7c790d92e..d8e00f31df6 100644
--- a/theories/Algebra/AbGroups/Cyclic.v
+++ b/theories/Algebra/AbGroups/Cyclic.v
@@ -1,6 +1,6 @@
 Require Import Basics Types WildCat.Core Truncations.Core
   AbelianGroup AbHom Centralizer AbProjective
-  Groups.FreeGroup AbGroups.Z BinInt.Core Spaces.Int.
+  Groups.FreeGroup AbGroups.Z Spaces.Int.
 
 (** * Cyclic groups *)
 
@@ -48,7 +48,7 @@ Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat)
 Proof.
   induction n as [|n H].
   1: easy.
-  refine (grp_pow_homo _ _ _ @ _); simpl.
+  refine (grp_pow_natural _ _ _ @ _); simpl.
   by rewrite grp_unit_r.
 Defined.
 
@@ -71,7 +71,7 @@ Defined.
 
 (** The map sending the generator to [1 : Int]. *)
 Definition Z1_to_Z `{Funext} : ab_Z1 $-> abgroup_Z
-  := Z1_rec (G:=abgroup_Z) 1%binint.
+  := Z1_rec (G:=abgroup_Z) 1%int.
 
 (** TODO:  Prove that [Z1_to_Z] is a group isomorphism. *)
 
diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index 6eb290a44b9..d476119a3f1 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -1,5 +1,5 @@
 Require Import Basics.
-Require Import Spaces.Pos.Core Spaces.BinInt.
+Require Import Spaces.Pos.Core Spaces.Int.
 Require Import Algebra.AbGroups.AbelianGroup.
 
 Local Set Universe Minimization ToSet.
@@ -8,17 +8,25 @@ Local Set Universe Minimization ToSet.
 
 (** See also Cyclic.v for a definition of the integers as the free group on one generator. *)
 
-Local Open Scope binint_scope.
+Local Open Scope int_scope.
 
-(** TODO: switch to [Int] *)
 Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
   snrapply Build_AbGroup.
-  - refine (Build_Group BinInt binint_add 0 binint_negation _); repeat split.
+  - refine (Build_Group Int int_add 0 int_neg _); repeat split.
     + exact _.
-    + exact binint_add_assoc.
-    + exact binint_add_0_r.
-    + exact binint_add_negation_l.
-    + exact binint_add_negation_r.
-  - exact binint_add_comm.
+    + exact int_add_assoc.
+    + exact int_add_0_r.
+    + exact int_add_neg_l.
+    + exact int_add_neg_r.
+  - exact int_add_comm.
+Defined.
+
+(** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. *)
+Definition grp_pow_homo {G : Group} (g : G)
+  : GroupHomomorphism abgroup_Z G.
+Proof.
+  snrapply Build_GroupHomomorphism.
+  1: exact (grp_pow g).
+  intros m n; apply grp_pow_add.
 Defined.
diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
index 6f07a6937f0..560effb9eae 100644
--- a/theories/Algebra/AbSES/SixTerm.v
+++ b/theories/Algebra/AbSES/SixTerm.v
@@ -211,7 +211,7 @@ Proof.
     apply moveR_equiv_V; symmetry.
     refine (ap f _ @ _).
     1: apply Z1_rec_beta.
-    exact (ab_mul_homo f n Z1_gen).
+    exact (ab_mul_natural f n Z1_gen).
   - (* we get rid of [equiv_Z1_hom] *)
     apply isexact_equiv_fiber.
     apply isexact_ext_cyclic_ab_iii.
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 1c5f643b672..39eca032333 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -476,100 +476,63 @@ End GroupMovement.
 
 (** ** Power operation *)
 
-(** For a given [n : nat] we can define the [n]th power of a group element. *)
+(** For a given [g : G] we can define the function [Int -> G] sending an integer to that power of [g]. *)
 Definition grp_pow {G : Group} (g : G) (n : Int) : G
-  := match n with
-     | posS n => nat_iter n (g *.) g
-     | zero => mon_unit
-     | negS n => nat_iter n ((- g) *.) (- g)
-     end.
-
-(** Any homomorphism respects [grp_pow]. *)
-Lemma grp_pow_homo {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
+  := int_iter (g *.) n mon_unit.
+
+(** Any homomorphism respects [grp_pow]. In other words, [fun g => grp_pow g n] is natural. *)
+Lemma grp_pow_natural {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
   : f (grp_pow g n) = grp_pow (f g) n.
 Proof.
-  induction n.
-  - apply grp_homo_unit.
-  - destruct n; simpl in IHn |- *.
-    + reflexivity.
-    + lhs snrapply grp_homo_op.
-      apply ap.
-      exact IHn.
-  - destruct n; simpl in IHn |- *.
-    + apply grp_homo_inv.
-    + lhs snrapply grp_homo_op.
-      apply ap011.
-      * apply grp_homo_inv.
-      * exact IHn.
+  lhs snrapply (int_iter_commute_map _ ((f g) *.)).
+  1: nrapply grp_homo_op.
+  apply (ap (int_iter _ n)), grp_homo_unit.
 Defined.
 
 (** All powers of the unit are the unit. *)
 Definition grp_pow_unit {G : Group} (n : Int)
   : grp_pow (G:=G) mon_unit n = mon_unit.
 Proof.
-  induction n.
+  snrapply (int_iter_invariant n _ (fun g => g = mon_unit)); cbn.
+  1, 2: apply paths_ind_r.
+  - apply grp_unit_r.
+  - lhs nrapply grp_unit_r. apply grp_inv_unit.
   - reflexivity.
-  - destruct n; simpl. 
-    + reflexivity.
-    + by lhs nrapply grp_unit_l.
-  - destruct n; simpl in IHn |- *.
-    + apply grp_inv_unit.
-    + destruct IHn^.
-      rhs_V apply (@grp_inv_unit G).
-      apply grp_unit_r.
 Defined.
 
 (** Note that powers don't preserve the group operation as it is not commutative. This does hold in an abelian group so such a result will appear later. *)
 
-(** Helper functions for [grp_pow_int_add]. This is how we can unfold [grp_pow] once. *)
+(** The next two results tell us how [grp_pow] unfolds. *)
+Definition grp_pow_succ {G : Group} (n : Int) (g : G)
+  : grp_pow g (n.+1)%int = g * grp_pow g n
+  := int_iter_succ_l _ _ _.
 
-Definition grp_pow_int_add_1 {G : Group} (n : Int) (g : G)
-  : grp_pow g (n.+1)%int = g * grp_pow g n.
-Proof.
-  induction n; simpl.
-  - exact (grp_unit_r g)^.
-  - destruct n; reflexivity.
-  - destruct n.
-    + apply (grp_inv_r g)^.
-    + rhs srapply associativity.
-      rewrite grp_inv_r. 
-      apply (grp_unit_l _)^.
-Defined.
+Definition grp_pow_pred {G : Group} (n : Int) (g : G)
+  : grp_pow g (n.-1)%int = (- g) * grp_pow g n
+  := int_iter_pred_l _ _ _.
 
-Definition grp_pow_int_sub_1 {G : Group} (n : Int) (g : G)
-  : grp_pow g (n.-1)%int = (- g) * grp_pow g n.
+(** [grp_pow] satisfies an additive law of exponents. *)
+Definition grp_pow_add {G : Group} (m n : Int) (g : G)
+  : grp_pow g (n + m)%int = grp_pow g n * grp_pow g m.
 Proof.
-  induction n; simpl.
-  - exact (grp_unit_r (-g))^.
-  - destruct n.
-    + apply (grp_inv_l g)^.
-    + rhs srapply associativity.
-      rewrite grp_inv_l.
-      apply (grp_unit_l _)^.
-  - destruct n; reflexivity.
+  lhs nrapply int_iter_add.
+  induction n; cbn.
+  1: exact (grp_unit_l _)^.
+  1: rewrite int_iter_succ_l, grp_pow_succ.
+  2: rewrite int_iter_pred_l, grp_pow_pred; cbn.
+  1,2 : rhs_V srapply associativity;
+        apply ap, IHn.
 Defined.
 
 (** [grp_pow] commutes negative exponents to powers of the inverse *)
-Definition grp_pow_int_sign_commute {G : Group} (n : Int) (g : G)
+Definition grp_pow_neg {G : Group} (n : Int) (g : G)
   : grp_pow g (int_neg n) = grp_pow (- g) n.
 Proof.
-  induction n.
+  lhs nrapply int_iter_neg.
+  destruct n.
+  - cbn. by rewrite grp_inv_inv.
+  - reflexivity.
   - reflexivity.
-  - destruct n; reflexivity.
-  - destruct n; simpl; rewrite grp_inv_inv; reflexivity.
-Defined.
-
-(** [grp_pow] satisfies a law of exponents. *)
-Definition grp_pow_int_add {G : Group} (m n : Int) (g : G)
-  : grp_pow g (n + m)%int = grp_pow g n * grp_pow g m.
-Proof.
-  induction n; cbn.
-  1: exact (grp_unit_l _)^.
-  1: rewrite int_add_succ_l, 2 grp_pow_int_add_1.
-  2: rewrite int_add_pred_l, 2 grp_pow_int_sub_1.
-  1,2: rhs_V srapply associativity; 
-       snrapply (ap (_ *.));
-       exact IHn.
 Defined.
 
 (** ** The category of Groups *)
diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index ee0a10a886e..61f74885f74 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -1,225 +1,65 @@
 Require Import Classes.interfaces.canonical_names.
 Require Import Algebra.AbGroups.
 Require Import Algebra.Rings.CRing.
-Require Import Spaces.BinInt Spaces.Pos.
+Require Import Spaces.Int Spaces.Pos.
 Require Import WildCat.Core.
 
-(** In this file we define the ring Z of integers. The underlying abelian group is already defined in Algebra.AbGroups.Z. Many of the ring axioms are proven and made opaque. Typically, everything inside IsCRing can be opaque since we will only ever rewrite along them and they are hprops. This also means we don't have to be too careful with how our proofs are structured. This allows us to freely use tactics such as rewrite. It would perhaps be possible to shorten many of the proofs here, but it would probably be unneeded due to the opacicty. *)
+(** * In this file we define the ring [cring_Z] of integers with underlying abelian group [abroup_Z] defined in Algebra.AbGroups.Z. We also define multiplication by an integer in a general ring, and show that [cring_Z] is initial. *)
 
 (** The ring of integers *)
 Definition cring_Z : CRing.
 Proof.
   snrapply Build_CRing'.
+  6: repeat split.
   - exact abgroup_Z.
-  - exact 1%binint.
-  - exact binint_mul.
-  - exact binint_mul_comm.
-  - exact binint_mul_add_distr_l.
-  - split.
-    + split.
-      * exact _.
-      * exact binint_mul_assoc.
-    + exact binint_mul_1_l.
-    + exact binint_mul_1_r.
+  - exact 1%int.
+  - exact int_mul.
+  - exact int_mul_comm.
+  - exact int_dist_l.
+  - exact _.
+  - exact int_mul_assoc.
+  - exact int_mul_1_l.
+  - exact int_mul_1_r.
 Defined.
 
 Local Open Scope mc_scope.
 
-(** Multiplication of a ring element by an integer. *)
-(** We call this a "catamorphism" which is the name of the map from an initial object. It seems to be a more common terminology in computer science. *)
-Definition cring_catamorphism_fun (R : CRing) (z : cring_Z) : R
-  := match z with
-     | neg z => pos_peano_rec R (-1) (fun n nr => -1 + nr) z
-     | 0%binint => 0
-     | pos z => pos_peano_rec R 1 (fun n nr => 1 + nr) z
-     end.
+(** Given a ring element [r], we get a map [Int -> R] sending an integer to that multiple of [r]. *)
+Definition rng_int_mult (R : Ring) := grp_pow_homo : R -> Int -> R.
 
-(** TODO: remove these (they will be cleaned up in the future)*)
-(** Left multiplication is an equivalence *)
-Local Instance isequiv_group_left_op {G} `{IsGroup G}
-  : forall (x : G), IsEquiv (fun t => sg_op x t).
+(** [rng_int_mult R 1] preserves multiplication.  This requires that the specified ring element is the unit. *)
+Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
+  : IsSemiGroupPreserving (A:=cring_Z) (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
 Proof.
-  intro x.
-  srapply isequiv_adjointify.
-  1: exact (sg_op (-x)).
-  all: intro y.
-  all: refine (associativity _ _ _ @ _ @ left_identity y).
-  all: refine (ap (fun x => x * y) _).
-  1: apply right_inverse.
-  apply left_inverse.
-Defined.
-
-(** Right multiplication is an equivalence *)
-Local Instance isequiv_group_right_op {G} `{IsGroup G}
-  : forall x:G, IsEquiv (fun y => sg_op y x).
-Proof.
-  intro x.
-  srapply isequiv_adjointify.
-  1: exact (fun y => sg_op y (- x)).
-  all: intro y.
-  all: refine ((associativity _ _ _)^ @ _ @ right_identity y).
-  all: refine (ap (y *.) _).
-  1: apply left_inverse.
-  apply right_inverse.
-Defined.
-
-(** Preservation of + *)
-Global Instance issemigrouppreserving_cring_catamorphism_fun_plus (R : CRing)
-  : IsSemiGroupPreserving (Aop:=cring_plus) (Bop:=cring_plus)
-      (cring_catamorphism_fun R : cring_Z -> R).
-Proof.
-  (** Unfortunately, due to how we have defined things we need to seperate this out into 9 cases. *)
-  hnf. intros [x| |x] [y| |y].
-  (** Some of these cases are easy however *)
-  2,5,8: cbn; by rewrite right_identity.
-  3,4: symmetry; apply left_identity.
-  (** This leaves us with four cases to consider *)
-  (** x < 0 , y < 0 *)
-  { change (cring_catamorphism_fun R ((neg x) + (neg y))%binint
-      = (cring_catamorphism_fun R (neg x)) + (cring_catamorphism_fun R (neg y))).
-    induction y as [|y IHy] using pos_peano_ind.
-    { simpl.
-      rewrite pos_add_1_r.
-      rewrite pos_peano_rec_beta_pos_succ.
-      apply commutativity. }
-    simpl.
-    rewrite pos_add_succ_r.
-    rewrite 2 pos_peano_rec_beta_pos_succ.
-    rewrite simple_associativity.
-    rewrite (commutativity _ (-1)).
-    rewrite <- simple_associativity.
-    f_ap. }
-  (** x < 0 , y > 0 *)
-  { cbn.
-    revert x.
-    induction y as [|y IHy] using pos_peano_ind; intro x.
-    { cbn.
-      induction x as [|x] using pos_peano_ind.
-      1: symmetry; cbn; apply left_inverse.
-      rewrite pos_peano_rec_beta_pos_succ.
-      rewrite binint_pos_sub_succ_r.
-      cbn; rewrite <- simple_associativity.
-      apply (rng_moveL_Vr (R:=R)).
-      apply commutativity. }
-    induction x as [|x IHx] using pos_peano_ind.
-    { rewrite binint_pos_sub_succ_l.
-      cbn; apply (rng_moveL_Vr (R:=R)).
-      by rewrite pos_peano_rec_beta_pos_succ. }
-    rewrite binint_pos_sub_succ_succ.
-    rewrite IHy.
-    rewrite 2 pos_peano_rec_beta_pos_succ.
-    rewrite (commutativity (-1)).
-    rewrite simple_associativity.
-    rewrite <- (simple_associativity _ _ 1).
-    rewrite left_inverse.
+  intros x y.
+  cbn; unfold sg_op.
+  induction x as [|x|x].
+  - simpl.
+    by rhs nrapply rng_mult_zero_l.
+  - rewrite int_mul_succ_l.
+    rewrite grp_pow_add.
+    rewrite grp_pow_succ.
+    rhs nrapply rng_dist_r.
+    rewrite rng_mult_one_l.
     f_ap.
-    symmetry.
-    apply right_identity. }
-  - cbn.
-    revert x.
-    induction y as [|y IHy] using pos_peano_ind; intro x.
-    { induction x as [|x] using pos_peano_ind.
-      1: symmetry; cbn; apply right_inverse.
-      rewrite pos_peano_rec_beta_pos_succ.
-      rewrite (commutativity 1).
-      rewrite <- simple_associativity.
-      rewrite binint_pos_sub_succ_l.
-      cbn; by rewrite right_inverse, right_identity. }
-    induction x as [|x IHx] using pos_peano_ind.
-    { rewrite binint_pos_sub_succ_r.
-      rewrite pos_peano_rec_beta_pos_succ.
-      rewrite simple_associativity.
-      cbn.
-      rewrite (right_inverse 1).
-      symmetry.
-      apply left_identity. }
-    rewrite binint_pos_sub_succ_succ.
-    rewrite IHy.
-    rewrite 2 pos_peano_rec_beta_pos_succ.
-    rewrite (commutativity 1).
-    rewrite simple_associativity.
-    rewrite <- (simple_associativity _ _ (-1)).
-    rewrite (right_inverse 1).
-    f_ap; symmetry.
-    apply right_identity.
-  - cbn.
-    induction y as [|y IHy] using pos_peano_ind.
-    { cbn.
-      rewrite pos_add_1_r.
-      rewrite pos_peano_rec_beta_pos_succ.
-      apply commutativity. }
-    rewrite pos_add_succ_r.
-    rewrite 2 pos_peano_rec_beta_pos_succ.
-    rewrite simple_associativity.
-    rewrite IHy.
-    rewrite simple_associativity.
-    rewrite (commutativity 1).
-    reflexivity.
-Qed.
-
-Lemma cring_catamorphism_fun_negate {R} x
-  : cring_catamorphism_fun R (- x) = - cring_catamorphism_fun R x.
-Proof.
-  snrapply (groups.preserves_negate _).
-  1-6: typeclasses eauto.
-  snrapply Build_IsMonoidPreserving.
-  1: exact _.
-  split.
+  - rewrite int_mul_pred_l.
+    rewrite grp_pow_add.
+    rewrite grp_pow_pred.
+    rhs nrapply rng_dist_r.
+    rewrite IHx.
+    f_ap.
+    lhs rapply (grp_homo_inv (grp_pow_homo 1)).
+    symmetry; apply rng_mult_negate.
 Defined.
 
-Lemma cring_catamorphism_fun_pos_mult {R} x y
-  : cring_catamorphism_fun R (pos x * pos y)%binint
-    = cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y).
-Proof.
-  revert y.
-  induction x as [|x IHx] using pos_peano_ind; intro y.
-  { symmetry.
-    apply left_identity. }
-  change (cring_catamorphism_fun R (pos (pos_succ x * y)%pos)
-    = cring_catamorphism_fun R (pos (pos_succ x)) * cring_catamorphism_fun R (pos y)).
-  rewrite pos_mul_succ_l.
-  refine (issemigrouppreserving_cring_catamorphism_fun_plus
-    R (pos (x * y)%pos) (pos y) @ _).
-  rewrite IHx.
-  transitivity ((1 + cring_catamorphism_fun R (pos x)) * cring_catamorphism_fun R (pos y)).
-  2: simpl; by rewrite pos_peano_rec_beta_pos_succ.
-  rewrite (rng_dist_r (A:=R)).
-  rewrite rng_mult_one_l.
-  apply commutativity.
-Qed.
-
-(** Preservation of * (multiplication) *)
-Global Instance issemigrouppreserving_cring_catamorphism_fun_mult (R : CRing)
-  : IsSemiGroupPreserving (Aop:=(.*.)) (Bop:=(.*.))
-      (cring_catamorphism_fun R : cring_Z -> R).
-Proof.
-  hnf. intros [x| |x] [y| |y].
-  2,5,8: symmetry; apply (rng_mult_zero_r (A:=R)).
-  3,4: cbn; symmetry; rewrite (commutativity 0); apply (rng_mult_zero_r (A:=R)).
-  { change (cring_catamorphism_fun R (pos (x * y)%pos)
-      = cring_catamorphism_fun R (- (pos x : cring_Z))
-        * cring_catamorphism_fun R (- (pos y : cring_Z))).
-    by rewrite 2 cring_catamorphism_fun_negate, cring_catamorphism_fun_pos_mult,
-      (rng_mult_negate_negate (A:=R)). }
-  { change (cring_catamorphism_fun R (- (pos (x * y)%pos : cring_Z))
-      = cring_catamorphism_fun R (- (pos x : cring_Z))
-        * cring_catamorphism_fun R (pos y)).
-    by rewrite 2 cring_catamorphism_fun_negate, cring_catamorphism_fun_pos_mult,
-      (rng_mult_negate_l (A:=R)). }
-  { change (cring_catamorphism_fun R (- (pos (x * y)%pos : cring_Z))
-      = cring_catamorphism_fun R (pos x)
-        * cring_catamorphism_fun R (- (pos y : cring_Z))).
-    by rewrite 2 cring_catamorphism_fun_negate, cring_catamorphism_fun_pos_mult,
-      (rng_mult_negate_r (A:=R)). }
-  apply cring_catamorphism_fun_pos_mult.
-Qed.
-
-(** This is a ring homomorphism *)
-Definition rng_homo_int (R : CRing) : cring_Z $-> R.
+(** [rng_int_mult R 1] is a ring homomorphism *)
+Definition rng_homo_int (R : Ring) : (cring_Z : Ring) $-> R.
 Proof.
   snrapply Build_RingHomomorphism.
-  1: exact (cring_catamorphism_fun R).
-  repeat split; exact _.
+  1: exact (rng_int_mult R 1).
+  repeat split.
+  1,2: exact _.
+  apply rng_plus_zero_r.
 Defined.
 
 (** The integers are the initial commutative ring *)
@@ -229,28 +69,19 @@ Proof.
   intro R.
   exists (rng_homo_int R).
   intros g x.
-  destruct x as [n| |p].
-  + induction n using pos_peano_ind.
-    { cbn. symmetry; rapply (rng_homo_minus_one (B:=R)). }
-    simpl.
-    rewrite pos_peano_rec_beta_pos_succ.
-    rewrite binint_neg_pos_succ.
-    unfold binint_pred.
-    rewrite binint_add_comm.
-    rewrite rng_homo_plus.
-    rewrite rng_homo_minus_one.
-    apply ap.
-    exact IHn.
-  + by rewrite 2 rng_homo_zero.
-  + induction p using pos_peano_ind.
-    { cbn. symmetry; rapply (rng_homo_one g). }
-    simpl.
-    rewrite pos_peano_rec_beta_pos_succ.
-    rewrite binint_pos_pos_succ.
-    unfold binint_succ.
-    rewrite binint_add_comm.
-    rewrite rng_homo_plus.
+  unfold rng_homo_int, rng_int_mult; cbn.
+  induction x as [|x|x].
+  - by rhs nrapply (grp_homo_unit g).
+  - rewrite grp_pow_succ.
+    change (x.+1%int) with (1 + x)%int.
+    rewrite (rng_homo_plus g 1 x).
     rewrite rng_homo_one.
-    apply ap.
-    exact IHp.
+    f_ap.
+  - rewrite grp_pow_pred.
+    rewrite IHx.
+    clear IHx.
+    rewrite <- (rng_homo_one g).
+    rewrite <- (rng_homo_negate g).
+    lhs_V nrapply (rng_homo_plus g).
+    f_ap.
 Defined.
diff --git a/theories/HIT/FreeIntQuotient.v b/theories/HIT/FreeIntQuotient.v
index 096248ad933..f80293dc40b 100644
--- a/theories/HIT/FreeIntQuotient.v
+++ b/theories/HIT/FreeIntQuotient.v
@@ -1,6 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
-Require Import Spaces.BinInt Spaces.Circle.
+Require Import Spaces.Int Spaces.Circle.
 Require Import Colimits.Coeq HIT.Flattening Truncations.Core Truncations.Connectedness.
 
 Local Open Scope path_scope.
@@ -16,8 +16,8 @@ Section FreeIntAction.
 
   (** A free action by [Int] is the same as a single autoequivalence [f] (the action of [1]) whose iterates are all pointwise distinct. *)
   Context (f : R <~> R)
-          (f_free : forall (r : R) (n m : BinInt),
-                      (binint_iter f n r = binint_iter f m r) -> (n = m)).
+          (f_free : forall (r : R) (n m : Int),
+                      (int_iter f n r = int_iter f m r) -> (n = m)).
 
   (** We can then define the quotient to be the coequalizer of [f] and the identity map.  This gives it the desired universal property for all types; it remains to show that this definition gives a set. *)
   Let RmodZ := Coeq f idmap.
diff --git a/theories/Homotopy/PinSn.v b/theories/Homotopy/PinSn.v
index a81b460163d..4b76b93f9fc 100644
--- a/theories/Homotopy/PinSn.v
+++ b/theories/Homotopy/PinSn.v
@@ -2,7 +2,7 @@ Require Import Basics Types.
 Require Import WildCat.
 Require Import Pointed.
 Require Import Truncations.Core Truncations.Connectedness.
-Require Import Spaces.BinInt Spaces.Circle Spaces.Spheres.
+Require Import Spaces.Int Spaces.Circle Spaces.Spheres.
 Require Import Algebra.AbGroups.
 Require Import Homotopy.HomotopyGroup.
 Require Import Homotopy.HSpaceS1.
diff --git a/theories/Spaces/Circle.v b/theories/Spaces/Circle.v
index 840b3392393..ba4bf1f75ea 100644
--- a/theories/Spaces/Circle.v
+++ b/theories/Spaces/Circle.v
@@ -2,7 +2,7 @@
 Require Import Basics Types.
 Require Import Pointed.Core Pointed.Loops Pointed.pEquiv.
 Require Import HSet.
-Require Import Spaces.Pos Spaces.BinInt.
+Require Import Spaces.Int.
 Require Import Colimits.Coeq.
 Require Import Truncations.Core Truncations.Connectedness.
 
@@ -90,11 +90,11 @@ Section EncodeDecode.
 
   (** First we define the type of codes, this is a type family over the circle. This can be thought of as the covering space by the homotopical real numbers. It is defined by mapping loop to the path given by univalence applied to the automorphism of the integers. We will show that the section of this family at [base] is equivalent to the loop space of the circle. Giving us an equivalence [base = base <~> Int]. *)
   Definition Circle_code : Circle -> Type
-    := Circle_rec Type BinInt (path_universe binint_succ).
+    := Circle_rec Type Int (path_universe int_succ).
 
   (** Transporting along [loop] gives us the successor automorphism on [Int]. *)
-  Definition transport_Circle_code_loop (z : BinInt)
-    : transport Circle_code loop z = binint_succ z.
+  Definition transport_Circle_code_loop (z : Int)
+    : transport Circle_code loop z = int_succ z.
   Proof.
     refine (transport_compose idmap Circle_code loop z @ _).
     unfold Circle_code; rewrite Circle_rec_beta_loop.
@@ -102,13 +102,13 @@ Section EncodeDecode.
   Defined.
 
   (** Transporting along [loop^] gives us the predecessor on [Int]. *)
-  Definition transport_Circle_code_loopV (z : BinInt)
-    : transport Circle_code loop^ z = binint_pred z.
+  Definition transport_Circle_code_loopV (z : Int)
+    : transport Circle_code loop^ z = int_pred z.
   Proof.
     refine (transport_compose idmap Circle_code loop^ z @ _).
     rewrite ap_V.
     unfold Circle_code; rewrite Circle_rec_beta_loop.
-    rewrite <- (path_universe_V binint_succ).
+    rewrite <- (path_universe_V int_succ).
     apply transport_path_universe.
   Defined.
 
@@ -125,52 +125,26 @@ Section EncodeDecode.
     refine (transport_arrow _ _ _ @ _).
     refine (transport_paths_r loop _ @ _).
     rewrite transport_Circle_code_loopV.
-    destruct z as [n| |n].
-    2: apply concat_Vp.
-    { rewrite <- binint_neg_pos_succ.
-      unfold loopexp, loopexp_pos.
-      rewrite pos_peano_ind_beta_pos_succ.
-      apply concat_pV_p. }
-    induction n as [|n nH] using pos_peano_ind.
-    1: apply concat_1p.
-    rewrite <- pos_add_1_r.
-    change (pos (n + 1)%pos)
-      with (binint_succ (pos n)).
-    rewrite binint_pred_succ.
-    cbn; rewrite pos_add_1_r.
-    unfold loopexp_pos.
-    rewrite pos_peano_ind_beta_pos_succ.
-    reflexivity.
+    rewrite loopexp_pred_r.
+    apply concat_pV_p.
   Defined.
 
   (** The non-trivial part of the proof that decode and encode are equivalences is showing that decoding followed by encoding is the identity on the fibers over [base]. *)
-  Definition Circle_encode_loopexp (z:BinInt)
+  Definition Circle_encode_loopexp (z : Int)
     : Circle_encode base (loopexp loop z) = z.
   Proof.
-    destruct z as [n | | n]; unfold Circle_encode.
-    - induction n using pos_peano_ind; simpl in *.
-      + refine (moveR_transport_V _ loop _ _ _).
-        by symmetry; apply transport_Circle_code_loop.
-      + unfold loopexp_pos.
-        rewrite pos_peano_ind_beta_pos_succ.
-        rewrite transport_pp.
-        refine (moveR_transport_V _ loop _ _ _).
-        refine (_ @ (transport_Circle_code_loop _)^).
-        refine (IHn @ _^).
-        rewrite binint_neg_pos_succ.
-        by rewrite binint_succ_pred.
+    induction z as [|n | n].
     - reflexivity.
-    - induction n using pos_peano_ind; simpl in *.
-      + by apply transport_Circle_code_loop.
-      + unfold loopexp_pos.
-        rewrite pos_peano_ind_beta_pos_succ.
-        rewrite transport_pp.
-        refine (moveR_transport_p _ loop _ _ _).
-        refine (_ @ (transport_Circle_code_loopV _)^).
-        refine (IHn @ _^).
-        rewrite <- pos_add_1_r.
-        change (binint_pred (binint_succ (pos n)) = pos n).
-        apply binint_pred_succ.
+    - rewrite loopexp_succ_r.
+      unfold Circle_encode in IHz |- *.
+      rewrite transport_pp.
+      rewrite IHz.
+      apply transport_Circle_code_loop.
+    - rewrite loopexp_pred_r.
+      unfold Circle_encode in IHz |- *.
+      rewrite transport_pp.
+      rewrite IHz.
+      apply transport_Circle_code_loopV.
   Defined.
 
   (** Now we put it together. *)
@@ -187,7 +161,7 @@ Section EncodeDecode.
   Defined.
 
   (** Finally giving us an equivalence between the loop space of the [Circle] and [Int]. *)
-  Definition equiv_loopCircle_int : (base = base) <~> BinInt
+  Definition equiv_loopCircle_int : (base = base) <~> Int
     := Build_Equiv _ _ (Circle_encode base) (Circle_encode_isequiv base).
 
 End EncodeDecode.
@@ -215,15 +189,15 @@ Proof.
   assert (q := merely_path_is0connected Circle base y).
   strip_truncations.
   destruct p, q.
-  refine (istrunc_equiv_istrunc (n := 0) BinInt equiv_loopCircle_int^-1).
+  refine (istrunc_equiv_istrunc (n := 0) Int equiv_loopCircle_int^-1).
 Defined.
 
 (** ** Iteration of equivalences *)
 
 (** If [P : Circle -> Type] is defined by a type [X] and an autoequivalence [f], then the image of [n : Int] regarded as in [base = base] is [iter_int f n]. *)
-Definition Circle_action_is_iter `{Univalence} X (f : X <~> X) (n : BinInt) (x : X)
+Definition Circle_action_is_iter `{Univalence} X (f : X <~> X) (n : Int) (x : X)
 : transport (Circle_rec Type X (path_universe f)) (equiv_loopCircle_int^-1 n) x
-  = binint_iter f n x.
+  = int_iter f n x.
 Proof.
   refine (_ @ loopexp_path_universe _ _ _).
   refine (transport_compose idmap _ _ _ @ _).
diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v
index c7327614602..da60ce1c189 100644
--- a/theories/Spaces/Int.v
+++ b/theories/Spaces/Int.v
@@ -1,4 +1,4 @@
-Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences.
+Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe.
 Require Basics.Numerals.Decimal.
 Require Import Spaces.Nat.Core.
 
@@ -140,6 +140,11 @@ Defined.
 (** By Hedberg's theorem, we have that the integers are a set. *)
 Global Instance ishset_int@{} : IsHSet Int := _.
 
+(** *** Pointedness *)
+
+(** We sometimes want to treat the integers as a pointed type with basepoint given by 0. *)
+Global Instance ispointed_int : IsPointed Int := 0.
+
 (** ** Operations *)
 
 (** *** Addition *)
@@ -526,3 +531,204 @@ Proof.
     rewrite <- int_mul_neg_l.
     by rewrite IHx.
 Defined.
+
+(** ** Iteration of equivalences *)
+
+(** *** Iteration by arbitrary integers *)
+
+(** Iteration by arbitrary integers requires the endofunction to be an equivalence, so that we can define a negative iteration by using its inverse. *)
+
+Definition int_iter {A} (f : A -> A) `{!IsEquiv f} (n : Int) : A -> A
+  := match n with
+      | negS n => fun x => nat_iter n.+1%nat f^-1 x
+      | zero => idmap
+      | posS n => fun x => nat_iter n.+1%nat f x
+     end.
+
+Definition int_iter_neg {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (- n) a = int_iter f^-1 n a.
+Proof.
+  by destruct n.
+Defined.
+
+Definition int_iter_succ_l {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (int_succ n) a = f (int_iter f n a).
+Proof.
+  induction n as [|n|n].
+  - reflexivity.
+  - by destruct n.
+  - rewrite int_pred_succ. 
+    destruct n.
+    all: symmetry; apply eisretr.
+Defined.
+
+Definition int_iter_succ_r {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (int_succ n) a = int_iter f n (f a).
+Proof.
+  induction n as [|n|n].
+  - reflexivity.
+  - destruct n.
+    1: reflexivity.
+    cbn; f_ap.
+  - destruct n.
+    1: symmetry; apply eissect.
+    rewrite int_pred_succ.
+    apply (ap f^-1).
+    rhs_V nrapply IHn.
+    by destruct n.
+Defined.
+
+Definition int_iter_pred_l {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (int_pred n) a = f^-1 (int_iter f n a).
+Proof.
+  (* Convert the problem to be a problem about [f^-1] and [-n]. *)
+  lhs_V exact (int_iter_neg f^-1 (n.-1) a).
+  rhs_V exact (ap f^-1 (int_iter_neg f^-1 n a)).
+  (* Then [int_iter_succ_l] applies, after changing [- n.-1] to [(-n).+1]. *)
+  rewrite int_neg_pred.
+  apply int_iter_succ_l.
+Defined.
+
+Definition int_iter_pred_r {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (int_pred n) a = int_iter f n (f^-1 a).
+Proof.
+  (* Convert the problem to be a problem about [f^-1] and [-n]. *)
+  lhs_V exact (int_iter_neg f^-1 (n.-1) a).
+  rhs_V exact (int_iter_neg f^-1 n (f^-1 a)).
+  (* Then [int_iter_succ_r] applies, after changing [- n.-1] to [(-n).+1]. *)
+  rewrite int_neg_pred.
+  apply int_iter_succ_r.
+Defined.
+
+Definition int_iter_add {A} (f : A -> A) `{IsEquiv _ _ f} (m n : Int)
+  : int_iter f (m + n) == int_iter f m o int_iter f n.
+Proof.
+  intros a.
+  induction m as [|m|m].
+  - reflexivity.
+  - rewrite int_add_succ_l.
+    rewrite 2 int_iter_succ_l.
+    f_ap.
+  - rewrite int_add_pred_l.
+    rewrite 2 int_iter_pred_l.
+    f_ap.
+Defined.
+
+(** If [g : A -> A'] commutes with automorphisms of [A] and [A'], then it commutes with iteration. *)
+Definition int_iter_commute_map {A A'} (f : A -> A) `{!IsEquiv f}
+  (f' : A' -> A') `{!IsEquiv f'}
+  (g : A -> A') (p : g o f == f' o g) (n : Int) (a : A)
+  : g (int_iter f n a) = int_iter f' n (g a).
+Proof.
+  induction n as [|n IHn|n IHn] in a |- *.
+  - reflexivity.
+  - rewrite 2 int_iter_succ_r.
+    rewrite IHn.
+    f_ap.
+  - rewrite 2 int_iter_pred_r.
+    rewrite IHn.
+    f_ap.
+    apply moveL_equiv_V.
+    lhs_V nrapply p.
+    f_ap.
+    apply eisretr.
+Defined.
+
+Definition int_iter_invariant (n : Int) {A} (f : A -> A) `{!IsEquiv f}
+  (P : A -> Type)
+  (Psucc : forall x, P x -> P (f x))
+  (Ppred : forall x, P x -> P (f^-1 x))
+  : forall x, P x -> P (int_iter f n x).
+Proof.
+  induction n as [|n IHn|n IHn]; intro x.
+  - exact idmap.
+  - intro H.
+    rewrite int_iter_succ_l.
+    apply Psucc, IHn, H.
+  - intro H.
+    rewrite int_iter_pred_l.
+    apply Ppred, IHn, H.
+Defined.
+
+(** ** Exponentiation of loops *)
+
+Definition loopexp {A : Type} {x : A} (p : x = x) (z : Int) : (x = x)
+  := int_iter (equiv_concat_r p x) z idpath.
+
+Definition loopexp_succ_r {A : Type} {x : A} (p : x = x) (z : Int)
+  : loopexp p z.+1 = loopexp p z @ p
+  := int_iter_succ_l _ _ _.
+
+Definition loopexp_pred_r {A : Type} {x : A} (p : x = x) (z : Int)
+  : loopexp p z.-1 = loopexp p z @ p^
+  := int_iter_pred_l _ _ _.
+
+Definition loopexp_succ_l {A : Type} {x : A} (p : x = x) (z : Int)
+  : loopexp p z.+1 = p @ loopexp p z.
+Proof.
+  lhs nrapply loopexp_succ_r.
+  induction z as [|z|z].
+  - nrapply concat_1p_p1.
+  - rewrite loopexp_succ_r.
+    rhs nrapply concat_p_pp.
+    f_ap.
+  - rewrite loopexp_pred_r.
+    lhs nrapply concat_pV_p.
+    rhs nrapply concat_p_pp.
+    by apply moveL_pV.
+Defined.
+
+Definition loopexp_pred_l {A : Type} {x : A} (p : x = x) (z : Int)
+  : loopexp p z.-1 = p^ @ loopexp p z.
+Proof.
+  rewrite loopexp_pred_r.
+  induction z as [|z|z].
+  - exact (concat_1p _ @ (concat_p1 _)^).
+  - rewrite loopexp_succ_r.
+    lhs nrapply concat_pp_V.
+    rhs nrapply concat_p_pp.
+    by apply moveL_pM.
+  - rewrite loopexp_pred_r.
+    rhs nrapply concat_p_pp.
+    f_ap.
+Defined.
+
+Definition ap_loopexp {A B} (f : A -> B) {x : A} (p : x = x) (z : Int)
+  : ap f (loopexp p z) = loopexp (ap f p) z.
+Proof.
+  nrapply int_iter_commute_map.
+  intro q; apply ap_pp.
+Defined.
+
+Definition loopexp_add {A : Type} {x : A} (p : x = x) m n
+  : loopexp p (m + n) = loopexp p m @ loopexp p n.
+Proof.
+  induction m as [|m|m].
+  - symmetry; apply concat_1p.
+  - rewrite int_add_succ_l.
+    rewrite 2 loopexp_succ_l.
+    by rewrite IHm, concat_p_pp.
+  - rewrite int_add_pred_l.
+    rewrite 2 loopexp_pred_l.
+    by rewrite IHm, concat_p_pp.
+Defined.
+
+(** Under univalence, exponentiation of loops corresponds to iteration of autoequivalences. *)
+
+Definition equiv_path_loopexp {A : Type} (p : A = A) (z : Int) (a : A)
+  : equiv_path A A (loopexp p z) a = int_iter (equiv_path A A p) z a.
+Proof.
+  refine (int_iter_commute_map _ _ (fun p => equiv_path A A p a) _ _ _).
+  intro q; cbn.
+  nrapply transport_pp.
+Defined.
+
+Definition loopexp_path_universe `{Univalence} {A : Type} (f : A <~> A)
+  (z : Int) (a : A)
+  : transport idmap (loopexp (path_universe f) z) a = int_iter f z a.
+Proof.
+  revert f. equiv_intro (equiv_path A A) p.
+  refine (_ @ equiv_path_loopexp p z a).
+  refine (ap (fun q => equiv_path A A (loopexp q z) a) _).
+  apply eissect.
+Defined.
diff --git a/theories/Spaces/Torus/TorusHomotopy.v b/theories/Spaces/Torus/TorusHomotopy.v
index 46bedc1da48..ef20a811351 100644
--- a/theories/Spaces/Torus/TorusHomotopy.v
+++ b/theories/Spaces/Torus/TorusHomotopy.v
@@ -4,7 +4,7 @@ Require Import Modalities.ReflectiveSubuniverse Truncations.Core.
 Require Import Algebra.AbGroups.
 Require Import Homotopy.HomotopyGroup.
 Require Import Homotopy.PinSn.
-Require Import Spaces.BinInt.Core Spaces.Circle.
+Require Import Spaces.Int Spaces.Circle.
 
 Require Import Spaces.Torus.Torus.
 Require Import Spaces.Torus.TorusEquivCircles.
@@ -55,7 +55,7 @@ Proof.
 Defined.
 
 (** Loop space of torus *)
-Theorem loops_torus `{Univalence} : loops T <~>* BinInt * BinInt.
+Theorem loops_torus `{Univalence} : loops T <~>* Int * Int.
 Proof.
   (* Since [T] is 1-truncated, [loops T] is 0-truncated, and is therefore equivalent to its 0-truncation. *)
   refine (_ o*E pequiv_ptr (n:=0)).