Revert "Merge branch 'fast-int-with-pl-and-ocr-instances' into ocr+pl-instances"

This reverts commit 47725ea, reversing
changes made to 561308e.

Author: LorenzoMolena

Cubical/Algebra/AbGroup/Instances/Int/Fast.agda

@@ -42,11 +42,6 @@ abs : ℤ → ℕ
 abs (pos n) = n
 abs (negsuc n) = suc n
 
-sign : ℤ → ℤ
-sign (pos zero) = pos zero
-sign (pos (suc n)) = pos (suc zero)
-sign (negsuc n) = negsuc zero
-
 _ℕ-_ : ℕ → ℕ → ℤ
 a ℕ- 0 = pos a
 0 ℕ- suc b = negsuc b

Cubical/Algebra/CommRing/Instances/Int/Fast.agda

@@ -2,8 +2,7 @@ module Cubical.Data.Int.Fast.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Data.Nat as ℕ hiding (_+_ ; _·_)
-open import Cubical.Data.Int.Base hiding (_ℕ-_ ; _+_ ; _-_ ; _·_ ; sumFinℤ ; sumFinℤId) public
-open import Cubical.Data.Fin.Inductive.Base
+open import Cubical.Data.Int.Base hiding (_ℕ-_ ; _+_ ; _-_ ; _·_) public
 
 infixl 7 _·_
 infixl 6 _+_ _-_
@@ -16,25 +15,18 @@ _ℕ-_ : ℕ → ℕ → ℤ
 m ℕ- n = ℕ-hlp (m ℕ.∸ n) (n ℕ.∸ m)
 
 _+_ : ℤ → ℤ → ℤ
-pos m    + pos n    = pos (m ℕ.+ n)
-negsuc m + negsuc n = negsuc (suc (m ℕ.+ n))
-pos m    + negsuc n = m ℕ- (suc n)
-negsuc m + pos n    = n ℕ- (suc m)
+pos n + pos n₁ = pos (n ℕ.+ n₁)
+negsuc n + negsuc n₁ = negsuc (suc (n ℕ.+ n₁))
+pos n + negsuc n₁ = n ℕ- (suc n₁)
+negsuc n + pos n₁ = n₁ ℕ- (suc n)
 
 _-_ : ℤ → ℤ → ℤ
 m - n = m + (- n)
 
 _·_ : ℤ → ℤ → ℤ
-pos m       · pos n       = pos (m ℕ.· n)
-pos zero    · negsuc n    = pos zero
-pos (suc m) · negsuc n    = negsuc (predℕ (suc m ℕ.· suc n))
-negsuc m    · pos zero    = pos zero
-negsuc m    · pos (suc n) = negsuc (predℕ (suc m ℕ.· suc n))
-negsuc m    · negsuc n    = pos (suc m ℕ.· suc n)
-
-sumFinℤ : {n : ℕ} (f : Fin n → ℤ) → ℤ
-sumFinℤ {n = n} f = sumFinGen {n = n} _+_ 0 f
-
-sumFinℤId : (n : ℕ) {f g : Fin n → ℤ}
-  → ((x : _) → f x ≡ g x) → sumFinℤ {n = n} f ≡ sumFinℤ {n = n} g
-sumFinℤId n t i = sumFinℤ {n = n} λ x → t x i
+pos n · pos n₁ = pos (n ℕ.· n₁)
+pos zero · negsuc n₁ = pos zero
+pos (suc n) · negsuc n₁ = negsuc (predℕ (suc n ℕ.· suc n₁))
+negsuc n · pos zero = pos zero
+negsuc n · pos (suc n₁) = negsuc (predℕ (suc n ℕ.· suc n₁))
+negsuc n · negsuc n₁ = pos (suc n ℕ.· suc n₁)