Rename, export and flip IsHom+

agda · Aug 25, 2023 · b628a4a · b628a4a
1 parent 49ff7c2
commit b628a4a
Showing 1 changed file with 48 additions and 47 deletions.
diff --git a/Cubical/Data/Int/MoreInts/QuoInt/Properties.agda b/Cubical/Data/Int/MoreInts/QuoInt/Properties.agda
@@ -241,69 +241,70 @@ private
   _+'_ : ℤ → ℤ → ℤ
   _+'_ = Iso.fun (binaryOpIso isoIntℤ) Int._+_
 
-  sucℤ→Int : ∀ (n : ℤ) → Int.sucℤ (ℤ→Int n) ≡ ℤ→Int (sucℤ n)
+  sucℤ→Int : ∀ (n : ℤ) → ℤ→Int (sucℤ n) ≡ Int.sucℤ (ℤ→Int n)
   sucℤ→Int (pos n) = refl
   sucℤ→Int (neg zero) = refl
   sucℤ→Int (neg (suc zero)) = refl
   sucℤ→Int (neg (suc (suc n))) = refl
   sucℤ→Int (posneg i) = refl
 
-  predℤ→Int : ∀ (n : ℤ) → Int.predℤ (ℤ→Int n) ≡ ℤ→Int (predℤ n)
+  predℤ→Int : ∀ (n : ℤ) → ℤ→Int (predℤ n) ≡ Int.predℤ (ℤ→Int n)
   predℤ→Int (pos zero) = refl
   predℤ→Int (pos (suc n)) = refl
   predℤ→Int (neg zero) = refl
   predℤ→Int (neg (suc n)) = refl
   predℤ→Int (posneg i) = refl
 
-  ℤ→Int+Int≡+ : ∀ (n m : ℤ) → (ℤ→Int n) Int.+ (ℤ→Int m) ≡ ℤ→Int (n + m)
-  ℤ→Int+Int≡+ n m = (ℤelim (λ n → ∀ (m : ℤ) → (ℤ→Int n) Int.+ (ℤ→Int m) ≡ ℤ→Int (n + m)) posℤ→Int+Int≡+ negsucℤ→Int+Int≡+ n) m
-    where
-    posℤ→Int+Int≡+ : ∀ (n : ℕ) (m : ℤ) → (ℤ→Int (pos n)) Int.+ (ℤ→Int m) ≡ ℤ→Int ((pos n) + m)
-    posℤ→Int+Int≡+ zero m =
-      (ℤ→Int (pos zero)) Int.+ (ℤ→Int m)
-        ≡⟨ sym (Int.pos0+ (ℤ→Int m)) ⟩
-      ℤ→Int m
-        ≡⟨ cong ℤ→Int (sym (+-zeroʳ spos m)) ⟩
-      ℤ→Int (m + pos zero)
-        ≡⟨ cong ℤ→Int (+-comm m (pos zero)) ⟩
-      ℤ→Int (pos zero + m) ∎
-    posℤ→Int+Int≡+ (suc n) m =
-      (ℤ→Int (pos (suc n))) Int.+ (ℤ→Int m)
-        ≡⟨ sym (Int.sucℤ+ (Int.pos n) (ℤ→Int m)) ⟩
-      Int.sucℤ ((Int.pos n) Int.+ (ℤ→Int m))
-        ≡⟨ cong Int.sucℤ (posℤ→Int+Int≡+ n m) ⟩
-      Int.sucℤ (ℤ→Int ((pos n) + m))
-        ≡⟨ sucℤ→Int ((pos n) + m) ⟩
-      ℤ→Int (sucℤ ((pos n) + m))
-        ≡⟨ cong ℤ→Int (sucℤ-+ˡ (pos n) m) ⟩
-      ℤ→Int ((pos (suc n)) + m) ∎
-
-    negsucℤ→Int+Int≡+ : ∀ (n : ℕ) (m : ℤ) → (ℤ→Int (neg (suc n))) Int.+ (ℤ→Int m) ≡ ℤ→Int ((neg (suc n)) + m)
-    negsucℤ→Int+Int≡+ zero m =
-      Int.negsuc zero Int.+ ℤ→Int m
-        ≡⟨ sym (Int.predℤ+ (Int.pos zero) (ℤ→Int m)) ⟩
-      Int.predℤ ((Int.pos zero) Int.+ (ℤ→Int m))
-        ≡⟨ cong Int.predℤ (posℤ→Int+Int≡+ zero m) ⟩
-      Int.predℤ (ℤ→Int ((neg zero) + m))
-        ≡⟨ predℤ→Int ((neg zero) + m) ⟩
-      ℤ→Int (predℤ ((neg zero) + m))
-        ≡⟨ cong ℤ→Int (predℤ-+ˡ (neg zero) m) ⟩
-      ℤ→Int ((neg (suc zero)) +  m) ∎
-    negsucℤ→Int+Int≡+ (suc n) m =
-      Int.negsuc (suc n) Int.+ ℤ→Int m
-        ≡⟨ sym (Int.predℤ+ (Int.negsuc n) (ℤ→Int m)) ⟩
-      Int.predℤ ((Int.negsuc n) Int.+ ℤ→Int m)
-        ≡⟨ cong Int.predℤ (negsucℤ→Int+Int≡+ n m) ⟩
-      Int.predℤ (ℤ→Int ((neg (suc n)) + m))
-        ≡⟨ predℤ→Int ((neg (suc n)) + m) ⟩
-      ℤ→Int (predℤ ((neg (suc n)) + m))
-        ≡⟨ cong ℤ→Int (predℤ-+ˡ (neg (suc n)) m) ⟩
-      ℤ→Int ((neg (suc (suc n))) + m) ∎
+ℤ→IntIsHom+ : ∀ (n m : ℤ) → ℤ→Int (n + m) ≡ (ℤ→Int n) Int.+ (ℤ→Int m)
+ℤ→IntIsHom+ n m = (ℤelim (λ n → ∀ (m : ℤ) → ℤ→Int (n + m) ≡ (ℤ→Int n) Int.+ (ℤ→Int m)) posℤ→Int+Int≡+ negsucℤ→Int+Int≡+ n) m
+  where
+  posℤ→Int+Int≡+ : ∀ (n : ℕ) (m : ℤ) → ℤ→Int ((pos n) + m) ≡ (ℤ→Int (pos n)) Int.+ (ℤ→Int m)
+  posℤ→Int+Int≡+ zero m =
+    ℤ→Int (pos zero + m)
+      ≡⟨ cong ℤ→Int (+-comm (pos zero) m) ⟩
+    ℤ→Int (m + pos zero)
+      ≡⟨ cong ℤ→Int (+-zeroʳ spos m) ⟩
+    ℤ→Int m
+      ≡⟨ Int.pos0+ (ℤ→Int m) ⟩
+    (ℤ→Int (pos zero)) Int.+ (ℤ→Int m) ∎
+  posℤ→Int+Int≡+ (suc n) m =
+    ℤ→Int ((pos (suc n)) + m)
+      ≡⟨ cong ℤ→Int (sym (sucℤ-+ˡ (pos n) m)) ⟩
+    ℤ→Int (sucℤ ((pos n) + m))
+      ≡⟨ sucℤ→Int ((pos n) + m) ⟩
+    Int.sucℤ (ℤ→Int ((pos n) + m))
+      ≡⟨ cong Int.sucℤ (posℤ→Int+Int≡+ n m) ⟩
+    Int.sucℤ ((Int.pos n) Int.+ (ℤ→Int m))
+      ≡⟨ Int.sucℤ+ (Int.pos n) (ℤ→Int m) ⟩
+    (ℤ→Int (pos (suc n))) Int.+ (ℤ→Int m) ∎
+
+  negsucℤ→Int+Int≡+ : ∀ (n : ℕ) (m : ℤ) → ℤ→Int ((neg (suc n)) + m) ≡ (ℤ→Int (neg (suc n))) Int.+ (ℤ→Int m)
+  negsucℤ→Int+Int≡+ zero m =
+    ℤ→Int ((neg (suc zero)) +  m)
+      ≡⟨ cong ℤ→Int (predℤ-+ˡ (neg zero) m) ⟩
+    ℤ→Int (predℤ ((neg zero) + m))
+      ≡⟨ predℤ→Int ((neg zero) + m) ⟩
+    Int.predℤ (ℤ→Int ((neg zero) + m))
+      ≡⟨ cong Int.predℤ (posℤ→Int+Int≡+ zero m) ⟩
+    Int.predℤ ((Int.pos zero) Int.+ (ℤ→Int m))
+      ≡⟨ Int.predℤ+ (Int.pos zero) (ℤ→Int m) ⟩
+    Int.negsuc zero Int.+ ℤ→Int m ∎
+  negsucℤ→Int+Int≡+ (suc n) m =
+    ℤ→Int ((neg (suc (suc n))) + m)
+      ≡⟨ cong ℤ→Int (predℤ-+ˡ (neg (suc n)) m) ⟩
+    ℤ→Int (predℤ ((neg (suc n)) + m))
+      ≡⟨ predℤ→Int ((neg (suc n)) + m) ⟩
+    Int.predℤ (ℤ→Int ((neg (suc n)) + m))
+      ≡⟨ cong Int.predℤ (negsucℤ→Int+Int≡+ n m) ⟩
+    Int.predℤ ((Int.negsuc n) Int.+ ℤ→Int m)
+      ≡⟨ Int.predℤ+ (Int.negsuc n) (ℤ→Int m) ⟩
+    Int.negsuc (suc n) Int.+ ℤ→Int m ∎
 
+private
   +'≡+ : _+'_ ≡ _+_
   +'≡+ =
     _+'_
-      ≡⟨ cong ( _∘_ (λ f → Int→ℤ ∘ f)) (funExt₂ ℤ→Int+Int≡+) ⟩
+      ≡⟨ sym (cong ( _∘_ (λ f → Int→ℤ ∘ f)) (funExt₂ ℤ→IntIsHom+)) ⟩
     (λ n → (λ m → (Int→ℤ (ℤ→Int (n + m)))))
       ≡⟨ funExt₂ (λ n m → (Iso.rightInv isoIntℤ (n + m))) ⟩
     _+_ ∎