{-# OPTIONS --cubical-compatible #-}
module Padova2025.Cubical.Issues.Quotients where

Quotients

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Equality.NaturalNumbers
open import Padova2025.ProvingBasics.Equality.Reasoning.Core

Let us define the type ℤ of integers.

infixl  _⊝_
data ℤ : Set where
  _⊝_ : ℕ → ℕ → ℤ

The idea is that an integer is represented by a pair, written a ⊝ b, of two natural numbers. We can image a to be credit and b to be debt. For instance, the negative number −2 can be represented as two ⊝ four, or as one ⊝ three.

We can then implement the successor and the predecessor function on the integers:

succℤ : ℤ → ℤ
succℤ (a ⊝ b) = succ a ⊝ b
-- increasing credit by one

predℤ : ℤ → ℤ
predℤ (a ⊝ b) = a ⊝ succ b
-- increasing debt by one

So far, so good; we could now go on and implement addition, multiplication and so on. However, we would run into a problem when verifying identities, such as succℤ (predℤ x) ≡ x: These aren’t true! While succℤ (predℤ x) represents the same integer as x does, these two values are not really the same. If x = a ⊝ b, then succℤ (predℤ x) is actually succ a ⊝ succ b.

Agda does not know which equivalence relation we have in mind; we have to define it on our own.

infix  _≈_
data _≈_ : ℤ → ℤ → Set where
  ≈-refl   : {x : ℤ}     → x ≈ x
  ≈-sym    : {x y : ℤ}   → x ≈ y → y ≈ x
  ≈-trans  : {x y z : ℤ} → x ≈ y → y ≈ z → x ≈ z
  ≈-cancel : {a b : ℕ}   → succ a ⊝ succ b ≈ a ⊝ b
-- the smallest equivalence relation generated by the constructor ≈-cancel

We can then state and prove the mentioned identity as follows.

succ-pred : (x : ℤ) → succℤ (predℤ x) ≈ x
succ-pred = {!!}

The type ℤ defined above is not really the type of integers; it is the type of integer representations. Each actual integer has infinitely many representations in the type ℤ, and we need to take care that we never compare such representations for actual equality _≡_ and instead always use our custom equivalence relation _≈_.

The true integers would arise from the misnamed type ℤ by a quotienting operation, where we formally identify values which are related by _≈_, along the following lines:

data ℤ' : Set  -- the actual type of integers
  _⊝_    : ℕ → ℕ → ℤ'
  cancel : (a b : ℕ) → succ a ⊝ succ b ≡ a ⊝ b
-- a dream in standard Agda, reality in Cubical Agda

However, this is not valid Agda code, hinting at a limitation of Agda’s type system: Standard Agda does not have quotient types—only Cubical Agda does.

Without proper quotient types, we have four options, described below but all of them not optimal. We should also remark that designing type-theoretic frameworks with sensible quotient types is an ongoing area of research with several intriguing projects, such as Cubical/Homotopy Type Theory, observational type theory, setoid type theory—and of course the minimalist foundation developed at the University of Padova.

Sticking to normal forms

Switching to an entirely different implementation

We can sidestep all issues with quotients by implementing the integers in a way with unique representations, for instance as follows.

data ℤ'' : Set where
  pos     : ℕ → ℤ''
  negsucc : ℕ → ℤ''

The idea is that pos x denotes the integer +x while negsucc x denotes the integer -(succ x).

Of course, this option of switching implementations is not available in general.

Postulating quotients

What Standard Agda does not have, we can postulate:

module PostulatedQuotient
  (X : Set)
  (_≈_ : X → X → Set)
  (≈-refl   : {x : X}     → x ≈ x)
  (≈-sym    : {x y : X}   → x ≈ y → y ≈ x)
  (≈-trans  : {x y z : X} → x ≈ y → y ≈ z → x ≈ z) where
  postulate
    Q           : Set
    [_]         : X → Q
    Q-eq        : {x y : X} → x ≈ y → [ x ] ≡ [ y ]
    Q-effective : {x y : X} → [ x ] ≡ [ y ] → x ≈ y
    elim
      : {R : Set} → (f : X → R) → (R-eq : {x y : X} → x ≈ y → f x ≡ f y)
      → (Q → R)
    elim-β
      : {R : Set} → (f : X → R) → (R-eq : {x y : X} → x ≈ y → f x ≡ f y)
      → (x : X) → elim f R-eq [ x ] ≡ f x
    -- and then also an induction principle for predicates Q → Set

open PostulatedQuotient ℤ _≈_ ≈-refl ≈-sym ≈-trans renaming (Q to ℤ''')

This approach works nicely if one only wants to use Agda as a language to describe what’s true in the platonic heaven of blackboard mathematics. But, as already described when we postulated function extensionality, postulates destroy desirable type-theoretic properties. Running proofs may get stuck on postulated terms, and proofs are cluttered by applications of elim-β. In a type system with native support for quotients, such as cubical type theory, (the equivalent of) elim f R-eq [ x ] would simply reduce to f x; instead of elim-β, we could have refl.

Entering setoid hell

An alternative course in Standard Agda is to enter setoid hell. This is the pet name for working with the unquotiented types such as ℤ above, but remembering (without tool support) to always prove (again without tool support) that functions preserve the custom equivalence relation.

For instance, in order to ensure that succℤ can be regarded as an function on actual integers instead of just their representations, we would need to prove the following:

succℤ-≈ : {x y : ℤ} → x ≈ y → succℤ x ≈ succℤ y
succℤ-≈ = {!!}

This is not too bad, and a similar proof obligation exists in Cubical Agda (which Cubical Agda will automatically remind us of). The proof has mathematical content, ensuring that succℤ doesn’t observably distinguish between equivalent representatives.

The more serious problem is that we need to remember and fulfill such proof obligations also in cases which are mathematically trivial. These cases require uninstructional boilerplate code.

For instance, let us define the double successsor function:

doublesuccℤ : ℤ → ℤ
doublesuccℤ x = succℤ (succℤ x)

As succℤ preserves the equivalence relation, so does doublesuccℤ. However, we need to explicitly state and prove this fact:

doublesuccℤ-≈ : {x y : ℤ} → x ≈ y → doublesuccℤ x ≈ doublesuccℤ y
doublesuccℤ-≈ = {!!}

Exercise: An explicit description of the equivalence relation

Above we have defined _≈_ as the reflexive symmetric transitive hull of the relation given just by the sole constructor ≈-cancel. This approach makes it easy to set up the equivalence relation and to show that elements are related; but showing that elements are not related requires more insight to the situation, such as an explicit description of the generated relation.

_≈'_ : ℤ → ℤ → Set
(a ⊝ b) ≈' (a' ⊝ b') = (a + b') ≡ (a' + b)

≈'-refl : {x : ℤ} → x ≈' x
≈'-refl = {!!}

≈'-sym : {x y : ℤ} → x ≈' y → y ≈' x
≈'-sym = {!!}

Beware that the following exercise requires some patience.

≈'-trans : {x y z : ℤ} → x ≈' y → y ≈' z → x ≈' z
≈'-trans = {!!}

≈→≈' : {x y : ℤ} → x ≈ y → x ≈' y
≈→≈' = {!!}

≈-cancel-more : (x a b : ℕ) → (x + a) ⊝ (x + b) ≈ a ⊝ b
≈-cancel-more = {!!}

≡→≈ : {x y : ℤ} → x ≡ y → x ≈ y
≡→≈ = {!!}

≈'→≈ : {x y : ℤ} → x ≈' y → x ≈ y
≈'→≈ = {!!}

zeroℤ : ℤ
zeroℤ = zero ⊝ zero

oneℤ : ℤ
oneℤ = one ⊝ zero

zeroℤ≉oneℤ : ¬ zeroℤ ≈ oneℤ
zeroℤ≉oneℤ = {!!}