Cubical.Data.Int.MoreInts.QuoInt.Properties

{-# OPTIONS --safe #-}
module Cubical.Data.Int.MoreInts.QuoInt.Properties where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Functions.FunExtEquiv
open import Cubical.Relation.Nullary

open import Cubical.Data.Nat as ℕ using (ℕ; zero; suc)
open import Cubical.Data.Bool as Bool using (Bool; not; notnot)
open import Cubical.Data.Empty
open import Cubical.Data.Unit renaming (Unit to ⊤)

import Cubical.Data.Int as Int
open import Cubical.Data.Int.MoreInts.QuoInt.Base renaming (elim to ℤelim)

·S-comm : ∀ x y → x ·S y ≡ y ·S x
·S-comm = Bool.⊕-comm

·S-assoc : ∀ x y z → x ·S (y ·S z) ≡ (x ·S y) ·S z
·S-assoc = Bool.⊕-assoc

not-·Sˡ : ∀ x y → not (x ·S y) ≡ not x ·S y
not-·Sˡ = Bool.not-⊕ˡ


snotz : ∀ s n s' → ¬ (signed s (suc n) ≡ signed s' zero)
snotz s n s' eq = subst (λ { (signed s (suc n)) → ⊤
                           ; _                  → ⊥ }) eq tt


+-zeroʳ : ∀ s m → m + signed s zero ≡ m
+-zeroʳ s (signed s' zero) = signed-zero s s'
+-zeroʳ s (pos (suc n)) = cong sucℤ  (+-zeroʳ s (pos n))
+-zeroʳ s (neg (suc n)) = cong predℤ (+-zeroʳ s (neg n))
+-zeroʳ spos (posneg i) j = posneg (i ∧ j)
+-zeroʳ sneg (posneg i) j = posneg (i ∨ ~ j)

+-identityʳ : ∀ m → m + pos zero ≡ m
+-identityʳ = +-zeroʳ spos

sucℤ-+ʳ : ∀ m n → sucℤ (m + n) ≡ m + sucℤ n
sucℤ-+ʳ (signed _ zero) _ = refl
sucℤ-+ʳ (posneg _) _ = refl
sucℤ-+ʳ (pos (suc m)) n = cong sucℤ (sucℤ-+ʳ (pos m) n)
sucℤ-+ʳ (neg (suc m)) n =
  sucPredℤ (neg m + n) ∙∙
  sym (predSucℤ (neg m + n)) ∙∙
  cong predℤ (sucℤ-+ʳ (neg m) n)

-- I wonder if we could somehow use negEq to get this for free from the above...
predℤ-+ʳ : ∀ m n → predℤ (m + n) ≡ m + predℤ n
predℤ-+ʳ (signed _ zero) _ = refl
predℤ-+ʳ (posneg _) _ = refl
predℤ-+ʳ (neg (suc m)) n = cong predℤ (predℤ-+ʳ (neg m) n)
predℤ-+ʳ (pos (suc m)) n =
  predSucℤ (pos m + n) ∙∙
  sym (sucPredℤ (pos m + n)) ∙∙
  cong sucℤ (predℤ-+ʳ (pos m) n)

+-comm : ∀ m n → m + n ≡ n + m
+-comm (signed s zero) n = sym (+-zeroʳ s n)
+-comm (pos (suc m)) n = cong sucℤ  (+-comm (pos m) n) ∙ sucℤ-+ʳ  n (pos m)
+-comm (neg (suc m)) n = cong predℤ (+-comm (neg m) n) ∙ predℤ-+ʳ n (neg m)
+-comm (posneg i) n = lemma n i
  where
  -- get some help from:
  -- https://www.codewars.com/kata/reviews/5c878e3ef1abb10001e32eb1/groups/5cca3f9e840f4b0001d8ac98
  lemma : ∀ n → (λ i → (posneg i + n) ≡ (n + posneg i))
          [ sym (+-zeroʳ spos n) ≡ sym (+-zeroʳ sneg n) ]
  lemma (pos zero) i j = posneg (i ∧ j)
  lemma (pos (suc n)) i = cong sucℤ (lemma (pos n) i)
  lemma (neg zero) i j = posneg (i ∨ ~ j)
  lemma (neg (suc n)) i = cong predℤ (lemma (neg n) i)
  lemma (posneg i) j k = posneg ((i ∧ ~ k) ∨ (i ∧ j) ∨ (j ∧ k))

sucℤ-+ˡ : ∀ m n → sucℤ (m + n) ≡ sucℤ m + n
sucℤ-+ˡ (pos _) n = refl
sucℤ-+ˡ (neg zero) n = refl
sucℤ-+ˡ (neg (suc m)) n = sucPredℤ _
sucℤ-+ˡ (posneg _) n = refl

-- I wonder if we could somehow use negEq to get this for free from the above...
predℤ-+ˡ : ∀ m n → predℤ (m + n) ≡ predℤ m + n
predℤ-+ˡ (pos zero) n = refl
predℤ-+ˡ (pos (suc m)) n = predSucℤ _
predℤ-+ˡ (neg _) n = refl
predℤ-+ˡ (posneg _) n = refl

+-assoc : ∀ m n o → m + (n + o) ≡ m + n + o
+-assoc (signed s zero) n o = refl
+-assoc (posneg i) n o = refl
+-assoc (pos (suc m)) n o = cong sucℤ  (+-assoc (pos m) n o) ∙ sucℤ-+ˡ  (pos m + n) o
+-assoc (neg (suc m)) n o = cong predℤ (+-assoc (neg m) n o) ∙ predℤ-+ˡ (neg m + n) o


sucℤ-inj : ∀ m n → sucℤ m ≡ sucℤ n → m ≡ n
sucℤ-inj m n p = sym (predSucℤ m) ∙ cong predℤ p ∙ predSucℤ n

predℤ-inj : ∀ m n → predℤ m ≡ predℤ n → m ≡ n
predℤ-inj m n p = sym (sucPredℤ m) ∙ cong sucℤ p ∙ sucPredℤ n

+-injˡ : ∀ o m n → o + m ≡ o + n → m ≡ n
+-injˡ (signed _ zero) _ _ p = p
+-injˡ (posneg _)      _ _ p = p
+-injˡ (pos (suc o)) m n p = +-injˡ (pos o) m n (sucℤ-inj  _ _ p)
+-injˡ (neg (suc o)) m n p = +-injˡ (neg o) m n (predℤ-inj _ _ p)

+-injʳ : ∀ m n o → m + o ≡ n + o → m ≡ n
+-injʳ m n o p = +-injˡ o m n (+-comm o m ∙ p ∙ +-comm n o)


·-comm : ∀ m n → m · n ≡ n · m
·-comm m n i = signed (·S-comm (sign m) (sign n) i) (ℕ.·-comm (abs m) (abs n) i)

·-identityˡ : ∀ n → pos 1 · n ≡ n
·-identityˡ n = cong (signed (sign n)) (ℕ.+-zero (abs n)) ∙ signed-inv n

·-identityʳ : ∀ n → n · pos 1 ≡ n
·-identityʳ n = ·-comm n (pos 1) ∙ ·-identityˡ n

·-zeroˡ : ∀ {s} n → signed s zero · n ≡ signed s zero
·-zeroˡ _ = signed-zero _ _

·-zeroʳ : ∀ {s} n → n · signed s zero ≡ signed s zero
·-zeroʳ n = cong (signed _) (sym (ℕ.0≡m·0 (abs n))) ∙ signed-zero _ _

·-signed-pos : ∀ {s} m n → signed s m · pos n ≡ signed s (m ℕ.· n)
·-signed-pos {s} zero n = ·-zeroˡ {s} (pos n)
·-signed-pos {s} (suc m) n i = signed (·S-comm s (sign-pos n i) i) (suc m ℕ.· n)


-- this proof is why we defined ℤ using `signed` instead of `pos` and `neg`
-- based on that in: https://github.com/danr/Agda-Numerics
·-assoc : ∀ m n o → m · (n · o) ≡ m · n · o

·-assoc (signed s zero) n o =
  ·-zeroˡ (n · o)
·-assoc m@(signed _ (suc _)) (signed s zero) o =
  ·-zeroʳ {sign o} m ∙ signed-zero _ _ ∙ cong (_· o) (sym (·-zeroʳ {s} m))
·-assoc m@(signed _ (suc _)) n@(signed _ (suc _)) (signed s zero) =
  cong (m ·_) (·-zeroʳ {s} n) ∙ ·-zeroʳ {s} m ∙ sym (·-zeroʳ {s} (m · n))

·-assoc (signed sm (suc m)) (signed sn (suc n)) (signed so (suc o)) i =
  signed (·S-assoc sm sn so i) (ℕ.·-assoc (suc m) (suc n) (suc o) i)

·-assoc (posneg i) n o j =
  isSet→isSet' isSetℤ (·-assoc (pos zero) n o) (·-assoc (neg zero) n o)
                      (λ i → posneg i · (n · o)) (λ i → posneg i · n · o) i j
·-assoc m@(signed _ (suc _)) (posneg i) o j =
  isSet→isSet' isSetℤ (·-assoc m (pos zero) o) (·-assoc m (neg zero) o)
                      (λ i → m · (posneg i · o)) (λ i → m · posneg i · o) i j
·-assoc m@(signed _ (suc _)) n@(signed _ (suc _)) (posneg i) j =
  isSet→isSet' isSetℤ (·-assoc m n (pos zero)) (·-assoc m n (neg zero))
                      (λ i → m · (n · posneg i)) (λ i → m · n · posneg i) i j


negateSuc : ∀ n → - sucℤ n ≡ predℤ (- n)
negateSuc n i = - sucℤ (negate-invol n (~ i))

negatePred : ∀ n → - predℤ n ≡ sucℤ (- n)
negatePred n i = negate-invol (sucℤ (- n)) i

negate-+ : ∀ m n → - (m + n) ≡  (- m) + (- n)
negate-+ (signed _ zero) n = refl
negate-+ (posneg _)      n = refl
negate-+ (pos (suc m))   n = negateSuc  (pos m + n) ∙ cong predℤ (negate-+ (pos m) n)
negate-+ (neg (suc m))   n = negatePred (neg m + n) ∙ cong sucℤ  (negate-+ (neg m) n)


negate-·ˡ : ∀ m n → - (m · n) ≡ (- m) · n
negate-·ˡ (signed _ zero) n = signed-zero (not (sign n)) (sign n)
negate-·ˡ (signed ss (suc m)) n i = signed (not-·Sˡ ss (sign n) i) (suc m ℕ.· abs n)
negate-·ˡ (posneg i) n j =
  isSet→isSet' isSetℤ (signed-zero (not (sign n)) _) (signed-zero _ _)
                      refl (λ i → posneg (~ i) · n) i j


signed-distrib : ∀ s m n → signed s (m ℕ.+ n) ≡ signed s m + signed s n
signed-distrib s zero n = refl
signed-distrib spos (suc m) n = cong sucℤ  (signed-distrib spos m n)
signed-distrib sneg (suc m) n = cong predℤ (signed-distrib sneg m n)

·-pos-suc : ∀ m n → pos (suc m) · n ≡ n + pos m · n
·-pos-suc m n = signed-distrib (sign n) (abs n) (m ℕ.· abs n)
                ∙ (λ i → signed-inv n i + signed (sign-pos m (~ i) ·S sign n) (m ℕ.· abs n))


-- the below is based on that in: https://github.com/danr/Agda-Numerics

·-distribˡ-pos : ∀ o m n → (pos o · m) + (pos o · n) ≡ pos o · (m + n)
·-distribˡ-pos zero m n = signed-zero (sign n) (sign (m + n))
·-distribˡ-pos (suc o) m n =
  pos (suc o) · m + pos (suc o) · n ≡[ i ]⟨ ·-pos-suc o m i + ·-pos-suc o n i ⟩
  m + pos o · m + (n + pos o · n)   ≡⟨ +-assoc (m + pos o · m) n (pos o · n) ⟩
  m + pos o · m + n + pos o · n     ≡[ i ]⟨ +-assoc m (pos o · m) n (~ i) + pos o · n ⟩
  m + (pos o · m + n) + pos o · n   ≡[ i ]⟨ m + +-comm (pos o · m) n i + pos o · n ⟩
  m + (n + pos o · m) + pos o · n   ≡[ i ]⟨ +-assoc m n (pos o · m) i + pos o · n ⟩
  m + n + pos o · m + pos o · n     ≡⟨ sym (+-assoc (m + n) (pos o · m) (pos o · n)) ⟩
  m + n + (pos o · m + pos o · n)   ≡⟨ cong ((m + n) +_) (·-distribˡ-pos o m n) ⟩
  m + n + pos o · (m + n)           ≡⟨ sym (·-pos-suc o (m + n)) ⟩
  pos (suc o) · (m + n) ∎

·-distribˡ-neg : ∀ o m n → (neg o · m) + (neg o · n) ≡ neg o · (m + n)
·-distribˡ-neg o m n =
     neg o · m  +    neg o · n  ≡[ i ]⟨ negate-·ˡ (pos o) m (~ i) + negate-·ˡ (pos o) n (~ i) ⟩
  - (pos o · m) + - (pos o · n) ≡⟨ sym (negate-+ (pos o · m) (pos o · n)) ⟩
  - (pos o · m + pos o · n)     ≡⟨ cong -_ (·-distribˡ-pos o m n) ⟩
  - (pos o · (m + n))           ≡⟨ negate-·ˡ (pos o) (m + n) ⟩
     neg o · (m + n)            ∎

·-distribˡ : ∀ o m n → (o · m) + (o · n) ≡ o · (m + n)
·-distribˡ (pos o) m n = ·-distribˡ-pos o m n
·-distribˡ (neg o) m n = ·-distribˡ-neg o m n
·-distribˡ (posneg i) m n j =
  isSet→isSet' isSetℤ (·-distribˡ-pos zero m n) (·-distribˡ-neg zero m n)
                      (λ i → posneg i · n) (λ i → posneg i · (m + n)) i j

·-distribʳ : ∀ m n o → (m · o) + (n · o) ≡ (m + n) · o
·-distribʳ m n o = (λ i → ·-comm m o i + ·-comm n o i) ∙ ·-distribˡ o m n ∙ ·-comm o (m + n)


sign-pos-suc-· : ∀ m n → sign (pos (suc m) · n) ≡ sign n
sign-pos-suc-· m (signed s zero) = sign-pos (suc m ℕ.· zero)
sign-pos-suc-· m (posneg i)      = sign-pos (suc m ℕ.· zero)
sign-pos-suc-· m (signed s (suc n)) = refl

·-injˡ : ∀ o m n → pos (suc o) · m ≡ pos (suc o) · n → m ≡ n
·-injˡ o m n p = sym (signed-inv m) ∙ (λ i → signed (sign-eq i) (abs-eq i)) ∙ signed-inv n
  where sign-eq = sym (sign-pos-suc-· o m) ∙ cong sign p ∙ sign-pos-suc-· o n
        abs-eq = ℕ.inj-sm· {o} (cong abs p)

·-injʳ : ∀ m n o → m · pos (suc o) ≡ n · pos (suc o) → m ≡ n
·-injʳ m n o p = ·-injˡ o m n (·-comm (pos (suc o)) m ∙ p ∙ ·-comm n (pos (suc o)))

private
  _+'_ : ℤ → ℤ → ℤ
  _+'_ = Iso.fun (binaryOpIso isoIntℤ) Int._+_

  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ℤ 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

ℤ→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
  +'≡+ : _+'_ ≡ _+_
  +'≡+ =
    _+'_
      ≡⟨ sym (cong (_∘_ (_∘_ Int→ℤ)) (funExt₂ ℤ→IntIsHom+)) ⟩
    (λ n → (λ m → (Int→ℤ (ℤ→Int (n + m)))))
      ≡⟨ funExt₂ (λ n m → (Iso.rightInv isoIntℤ (n + m))) ⟩
    _+_ ∎

  op≡Intℤ : (Int.ℤ → Int.ℤ → Int.ℤ) ≡ (ℤ → ℤ → ℤ)
  op≡Intℤ = isoToPath (binaryOpIso isoIntℤ)

  +Int≡+' : (λ i → op≡Intℤ i) [ Int._+_ ≡ _+'_ ]
  +Int≡+' = transport-filler op≡Intℤ Int._+_

+Int≡+ : (λ i → (op≡Intℤ ∙ refl) i) [ Int._+_ ≡ _+_ ]
+Int≡+ = compPathP +Int≡+' +'≡+

ℤ→IntIsHom- : ∀ (n : ℤ) → ℤ→Int (- n) ≡ Int.- (ℤ→Int n)
ℤ→IntIsHom- n = ℤelim (λ n → ℤ→Int (- n) ≡ Int.- (ℤ→Int n)) posℤ→Int-Int≡- negsucℤ→Int-Int≡- n
  where
  posℤ→Int-Int≡- : ∀ (n : ℕ) → ℤ→Int (- (pos n)) ≡ Int.- (ℤ→Int (pos n))
  posℤ→Int-Int≡- zero = refl
  posℤ→Int-Int≡- (suc n) = refl

  negsucℤ→Int-Int≡- : ∀ (n : ℕ) → ℤ→Int (- (neg (suc n))) ≡ Int.- (ℤ→Int (neg (suc n)))
  negsucℤ→Int-Int≡- zero = refl
  negsucℤ→Int-Int≡- (suc n) = refl

private
  -'_ : ℤ → ℤ
  -'_ = Iso.fun (endoIso isoIntℤ) (Int.-_)

  -'≡- : -'_ ≡ -_
  -'≡- =
    -'_
      ≡⟨ sym (cong (_∘_ Int→ℤ) (funExt ℤ→IntIsHom-)) ⟩
    (λ n → (Int→ℤ (ℤ→Int (- n))))
      ≡⟨ funExt (λ n → (Iso.rightInv isoIntℤ (- n))) ⟩
    -_ ∎

  endo≡Intℤ : (Int.ℤ → Int.ℤ) ≡ (ℤ → ℤ)
  endo≡Intℤ = isoToPath (endoIso isoIntℤ)

  -Int≡-' : (λ i → endo≡Intℤ i) [ Int.-_ ≡ -'_ ]
  -Int≡-' = transport-filler endo≡Intℤ (Int.-_)

-Int≡- : (λ i → (endo≡Intℤ ∙ refl) i) [ Int.-_ ≡ -_ ]
-Int≡- = compPathP -Int≡-' -'≡-

ℤ→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)
      ≡⟨ sym (cong ℤ→Int (sym (·-zeroˡ {s = spos} m))) ⟩
    (ℤ→Int (pos zero)) Int.· (ℤ→Int m) ∎
  posℤ→Int·Int≡· (suc n) m =
    ℤ→Int ((pos (suc n)) · m)
      ≡⟨ cong ℤ→Int (·-pos-suc n m) ⟩
    ℤ→Int (m + ((pos n) · m))
      ≡⟨ ℤ→IntIsHom+ m ((pos n) · m) ⟩
    (ℤ→Int m) Int.+ ℤ→Int ((pos n) · m)
      ≡⟨ cong (λ k → (ℤ→Int m) Int.+ k) (posℤ→Int·Int≡· n 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 (λ k → ℤ→Int (- k)) (·-identityˡ m) ⟩
    ℤ→Int (- m)
      ≡⟨ ℤ→IntIsHom- m ⟩
    (ℤ→Int (neg (suc zero))) Int.· (ℤ→Int m) ∎
  negsucℤ→Int·Int≡· (suc n) m =
    ℤ→Int ((neg (suc (suc n))) · m)
      ≡⟨ cong ℤ→Int (sym (·-distribʳ (neg (suc zero)) (neg (suc n)) m)) ⟩
    ℤ→Int (((neg (suc zero)) · m) + ((neg (suc n)) · m))
      ≡⟨ cong ( (λ k → ℤ→Int ((- k) + ((neg (suc n)) · m)))) (·-identityˡ m) ⟩
    ℤ→Int ((- m) + ((neg (suc n)) · m))
      ≡⟨ ℤ→IntIsHom+ (- m) ((neg (suc n)) · m) ⟩
    (ℤ→Int (- m)) Int.+ (ℤ→Int ((neg (suc n)) · m))
      ≡⟨ cong (λ k → k Int.+ (ℤ→Int ((neg (suc n)) · m))) (ℤ→IntIsHom- m) ⟩
    Int.- (ℤ→Int m) Int.+ (ℤ→Int ((neg (suc n)) · m))
      ≡⟨ cong (λ k → Int.- (ℤ→Int m) Int.+ k) (negsucℤ→Int·Int≡· n m) ⟩
    (ℤ→Int (neg (suc (suc n)))) Int.· (ℤ→Int m) ∎

private
  _·'_ : ℤ → ℤ → ℤ
  _·'_ = Iso.fun (binaryOpIso isoIntℤ) Int._·_

  ·'≡· : _·'_ ≡ _·_
  ·'≡· =
    _·'_
      ≡⟨ sym (cong (_∘_ (_∘_ Int→ℤ)) (funExt₂ ℤ→IntIsHom·)) ⟩
    (λ n → (λ m → (Int→ℤ (ℤ→Int (n · m)))))
      ≡⟨ funExt₂ (λ n m → (Iso.rightInv isoIntℤ (n · m))) ⟩
    _·_ ∎

  ·Int≡·' : (λ i → op≡Intℤ i) [ Int._·_ ≡ _·'_ ]
  ·Int≡·' = transport-filler op≡Intℤ Int._·_

·Int≡· : (λ i → (op≡Intℤ ∙ refl) i) [ Int._·_ ≡ _·_ ]
·Int≡· = compPathP ·Int≡·' ·'≡·