```------------------------------------------------------------------------
-- The Agda standard library
--
-- Example of a Quotient: ℤ as (ℕ × ℕ / ∼)
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Relation.Binary.HeterogeneousEquality.Quotients.Examples where

open import Relation.Binary.HeterogeneousEquality.Quotients
open import Level using (0ℓ)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.HeterogeneousEquality hiding (isEquivalence)
import Relation.Binary.PropositionalEquality.Core as ≡
open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Product.Base using (_×_; _,_)
open import Function.Base

open ≅-Reasoning

ℕ² = ℕ × ℕ

_∼_ : ℕ² → ℕ² → Set
(x , y) ∼ (x′ , y′) = x + y′ ≅ x′ + y

infix 10 _∼_

∼-trans : ∀ {i j k} → i ∼ j → j ∼ k → i ∼ k
∼-trans {x₁ , y₁} {x₂ , y₂} {x₃ , y₃} p q =
≡-to-≅ \$ +-cancelˡ-≡ y₂ _ _ \$ ≅-to-≡ \$ begin
y₂ + (x₁ + y₃) ≡⟨ ≡.sym (+-assoc y₂ x₁ y₃) ⟩
y₂ + x₁ + y₃   ≡⟨ ≡.cong (_+ y₃) (+-comm y₂ x₁) ⟩
x₁ + y₂ + y₃   ≅⟨ cong (_+ y₃) p ⟩
x₂ + y₁ + y₃   ≡⟨ ≡.cong (_+ y₃) (+-comm x₂ y₁) ⟩
y₁ + x₂ + y₃   ≡⟨ +-assoc y₁ x₂ y₃ ⟩
y₁ + (x₂ + y₃) ≅⟨ cong (y₁ +_) q ⟩
y₁ + (x₃ + y₂) ≡⟨ +-comm y₁ (x₃ + y₂) ⟩
x₃ + y₂ + y₁   ≡⟨ ≡.cong (_+ y₁) (+-comm x₃ y₂) ⟩
y₂ + x₃ + y₁   ≡⟨ +-assoc y₂ x₃ y₁ ⟩
y₂ + (x₃ + y₁) ∎

∼-isEquivalence : IsEquivalence _∼_
∼-isEquivalence = record
{ refl  = refl
; sym   = sym
; trans = λ {i} {j} {k} → ∼-trans {i} {j} {k}
}

ℕ²-∼-setoid : Setoid 0ℓ 0ℓ
ℕ²-∼-setoid = record { isEquivalence = ∼-isEquivalence }

module Integers (quot : Quotients 0ℓ 0ℓ) where

Int : Quotient ℕ²-∼-setoid
Int = quot _

open Quotient Int renaming (Q to ℤ)

infixl 6 _+²_

_+²_ : ℕ² → ℕ² → ℕ²
(x₁ , y₁) +² (x₂ , y₂) = x₁ + x₂ , y₁ + y₂

+²-cong : ∀{a b a′ b′} → a ∼ a′ → b ∼ b′ → (a +² b) ∼ (a′ +² b′)
+²-cong {a₁ , b₁} {c₁ , d₁} {a₂ , b₂} {c₂ , d₂} ab∼cd₁ ab∼cd₂ = begin
(a₁ + c₁) + (b₂ + d₂) ≡⟨ ≡.cong (_+ (b₂ + d₂)) (+-comm a₁ c₁) ⟩
(c₁ + a₁) + (b₂ + d₂) ≡⟨ +-assoc c₁ a₁ (b₂ + d₂) ⟩
c₁ + (a₁ + (b₂ + d₂)) ≡⟨ ≡.cong (c₁ +_) (≡.sym (+-assoc a₁ b₂ d₂)) ⟩
c₁ + (a₁ + b₂ + d₂)   ≅⟨ cong (λ n → c₁ + (n + d₂)) ab∼cd₁ ⟩
c₁ + (a₂ + b₁ + d₂)   ≡⟨ ≡.cong (c₁ +_) (+-assoc a₂ b₁ d₂) ⟩
c₁ + (a₂ + (b₁ + d₂)) ≡⟨ ≡.cong (λ n → c₁ + (a₂ + n)) (+-comm b₁ d₂) ⟩
c₁ + (a₂ + (d₂ + b₁)) ≡⟨ ≡.sym (+-assoc c₁ a₂ (d₂ + b₁)) ⟩
(c₁ + a₂) + (d₂ + b₁) ≡⟨ ≡.cong (_+ (d₂ + b₁)) (+-comm c₁ a₂) ⟩
(a₂ + c₁) + (d₂ + b₁) ≡⟨ +-assoc a₂ c₁ (d₂ + b₁) ⟩
a₂ + (c₁ + (d₂ + b₁)) ≡⟨ ≡.cong (a₂ +_) (≡.sym (+-assoc c₁ d₂ b₁)) ⟩
a₂ + (c₁ + d₂ + b₁)   ≅⟨ cong (λ n → a₂ + (n + b₁)) ab∼cd₂ ⟩
a₂ + (c₂ + d₁ + b₁)   ≡⟨ ≡.cong (a₂ +_) (+-assoc c₂ d₁ b₁) ⟩
a₂ + (c₂ + (d₁ + b₁)) ≡⟨ ≡.cong (λ n → a₂ + (c₂ + n)) (+-comm d₁ b₁) ⟩
a₂ + (c₂ + (b₁ + d₁)) ≡⟨ ≡.sym (+-assoc a₂ c₂ (b₁ + d₁)) ⟩
(a₂ + c₂) + (b₁ + d₁) ∎

module _ (ext : ∀ {a b} {A : Set a} {B₁ B₂ : A → Set b} {f₁ : ∀ a → B₁ a}
{f₂ : ∀ a → B₂ a} → (∀ a → f₁ a ≅ f₂ a) → f₁ ≅ f₂) where

infixl 6 _+ℤ_

_+ℤ_ : ℤ → ℤ → ℤ
_+ℤ_ = Properties₂.lift₂ ext Int Int (λ i j → abs (i +² j))
\$ λ {a} {b} {c} p p′ → compat-abs (+²-cong {a} {b} {c} p p′)

zero² : ℕ²
zero² = 0 , 0

zeroℤ : ℤ
zeroℤ = abs zero²

+²-identityʳ : (i : ℕ²) → (i +² zero²) ∼ i
+²-identityʳ (x , y) = begin
(x + 0) + y ≡⟨ ≡.cong (_+ y) (+-identityʳ x) ⟩
x + y       ≡⟨ ≡.cong (x +_) (≡.sym (+-identityʳ y)) ⟩
x + (y + 0) ∎

+ℤ-on-abs≅abs-+₂ : ∀ a b → abs a +ℤ abs b ≅ abs (a +² b)
+ℤ-on-abs≅abs-+₂ = Properties₂.lift₂-conv ext Int Int _
\$ λ {a} {b} {c} p p′ → compat-abs (+²-cong {a} {b} {c} p p′)

+ℤ-identityʳ : ∀ i → i +ℤ zeroℤ ≅ i
+ℤ-identityʳ = lift _ eq (≅-heterogeneous-irrelevantʳ _ _ ∘ compat-abs) where

eq : ∀ a → abs a +ℤ zeroℤ ≅ abs a
eq a = begin
abs a +ℤ zeroℤ      ≡⟨⟩
abs a +ℤ abs zero²  ≅⟨ +ℤ-on-abs≅abs-+₂ a zero² ⟩
abs (a +² zero²)    ≅⟨ compat-abs (+²-identityʳ a) ⟩
abs a               ∎

+²-identityˡ : (i : ℕ²) → (zero² +² i) ∼ i
+²-identityˡ i = refl

+ℤ-identityˡ : (i : ℤ)  → zeroℤ +ℤ i ≅ i
+ℤ-identityˡ = lift _ eq (≅-heterogeneous-irrelevantʳ _ _ ∘ compat-abs) where

eq : ∀ a → zeroℤ +ℤ abs a ≅ abs a
eq a = begin
zeroℤ +ℤ abs a     ≡⟨⟩
abs zero² +ℤ abs a ≅⟨ +ℤ-on-abs≅abs-+₂ zero² a ⟩
abs (zero² +² a)   ≅⟨ compat-abs (+²-identityˡ a) ⟩
abs a              ∎

+²-assoc : (i j k : ℕ²) → ((i +² j) +² k) ∼ (i +² (j +² k))
+²-assoc (a , b) (c , d) (e , f) = begin
((a + c) + e) + (b + (d + f)) ≡⟨ ≡.cong (_+ (b + (d + f))) (+-assoc a c e) ⟩
(a + (c + e)) + (b + (d + f)) ≡⟨ ≡.cong ((a + (c + e)) +_) (≡.sym (+-assoc b d f)) ⟩
(a + (c + e)) + ((b + d) + f) ∎

+ℤ-assoc : ∀ i j k → (i +ℤ j) +ℤ k ≅ i +ℤ (j +ℤ k)
+ℤ-assoc = Properties₃.lift₃ ext Int Int Int eq compat₃ where

eq : ∀ i j k → (abs i +ℤ abs j) +ℤ abs k ≅ abs i +ℤ (abs j +ℤ abs k)
eq i j k = begin
(abs i +ℤ abs j) +ℤ abs k ≅⟨ cong (_+ℤ abs k) (+ℤ-on-abs≅abs-+₂ i j) ⟩
(abs (i +² j) +ℤ abs k)   ≅⟨ +ℤ-on-abs≅abs-+₂ (i +² j) k ⟩
abs ((i +² j) +² k)       ≅⟨ compat-abs (+²-assoc i j k) ⟩
abs (i +² (j +² k))       ≅⟨ sym (+ℤ-on-abs≅abs-+₂ i (j +² k)) ⟩
(abs i +ℤ abs (j +² k))   ≅⟨ cong (abs i +ℤ_) (sym (+ℤ-on-abs≅abs-+₂ j k)) ⟩
abs i +ℤ (abs j +ℤ abs k) ∎

compat₃ : ∀ {a a′ b b′ c c′} → a ∼ a′ → b ∼ b′ → c ∼ c′ → eq a b c ≅ eq a′ b′ c′
compat₃ p q r = ≅-heterogeneous-irrelevantˡ _ _
\$ cong₂ _+ℤ_ (cong₂ _+ℤ_ (compat-abs p) (compat-abs q))
\$ compat-abs r
```