The quotient map is the identity function

Universal algebra is about quotients. Kernels, the isomorphism theorems, subdirect representation, the Birkhoff HSP theorem, etc. Every one of these takes the quotient of an algebra by a congruence. So a formalization of the subject, in a language with no quotient types, has to answer what 𝑨 ╱ θ means.

agda-algebras answers this question, twice. Each of two trees in that repository provides its own answer, and a comparison of the two is the most useful thing I could hand another practitioner, because it is concretely exhibited, rather than abstractly argued.

The constraint

Outside of the cubical fragment, Agda has no native quotient types. You cannot form "the type of θ-classes" and have its equality be: x ≡ y iff x θ y.

The agda-algebras library runs under --safe --cubical-compatible and postulates nothing, so the usual escape hatch, function extensionality (pointwise equal functions are equal), is also unavailable.

There are two ways out. Build the classes as objects, or stop insisting that equality is _≡_.

What the first way costs

The library's original tree, now frozen under Legacy/, builds the classes. A block is a predicate with a designated representative, and the quotient of a type is the type of blocks (src/Legacy/Base/Relations/Quotients.lagda.md):

record IsBlock  {A : Type a}{ρ : Level}
                (P : Pred A ρ){R : BinRel A ρ} : Type(a ⊔ suc ρ) where
 constructor mkblk
 field
  blk : A
  P≡[blk] : P ≡ [ blk ]{ρ} R

_/_ : (A : Type a){ρ : Level} → BinRel A ρ → Type(a ⊔ suc ρ)
A / R = Σ[ P ∈ Pred A _ ] IsBlock P {R}

The quotient algebra follows in src/Legacy/Base/Algebras/Congruences.lagda.md, and its type is where the first cost is visible:

_╱_ : (𝑨 : Algebra α) → Con{α}{ρ} 𝑨 → Algebra (α ⊔ suc ρ)

Algebra α in, Algebra (α ⊔ suc ρ) out. A quotient of an algebra is not an algebra at the same level, because a type of predicates lives above the type they are predicates on, and Agda's universes are not cumulative. Every theorem that quantifies over an algebra and its quotient now has two levels in it, and the level arithmetic is the reader's problem forever.

The second cost is in the operations, and it is the body of that same definition. To apply an operation to a tuple of blocks it picks each block's representative, IsBlock.blk, applies the original operation to those, and takes the class of the result. That is well defined only because the representatives were designated when the blocks were built, and proving anything about it means proving that the choice did not matter.

The third cost is the one that decided it. Facts about these quotients arrive carrying a hypothesis:

𝟎[_╱_] :  {α : Level}(𝑨 : Algebra α){ρ : Level}(θ : Con {α}{ρ}𝑨)
 →        swelldef 𝓥 (α ⊔ suc ρ)  → Con (𝑨 ╱ θ)

That swelldef argument is a weakened function extensionality, defined in the same tree, in src/Legacy/Base/Equality/Welldefined.lagda.md:

swelldef : ∀ ι α → Type (suc (α ⊔ ι))
swelldef ι α =  ∀ {I : Type ι}{A : Type α}(f : Op I A)(u v : I → A)
 →              u ≈ v → f u ≡ f v

funext→swelldef : {α 𝓥 : Level} → funext 𝓥 α → swelldef 𝓥 α

It follows from function extensionality, and the same module proves that at one choice of levels it implies function extensionality back. So the axiom the library refuses to postulate has become an argument threaded through the statements instead, which is more honest and no cheaper. The tree's own comment on one of its elimination rules is the fairest summary anyone has written of this approach: it "cheats a lot by baking in a large amount of extensionality that is miraculously true".

Setoids: the second answer

In the canonical Setoid tree, every structure needing equality carries its own equivalence relation. An algebra is a setoid, a carrier with an equivalence relation on it, together with an interpretation of each operation symbol as a function bundled with a proof that it respects the equivalence relation. A congruence is an equivalence relation on the carrier that contains the setoid equality and is compatible with the operations.

Then the quotient of a setoid keeps the carrier and swaps the equality (Setoid.Relations.Quotients):

_/_ : (A : Type α) → Equivalence A{ℓ} → Setoid _ _
A / R = record { Carrier = A ; _≈_ = (proj₁ R) ; isEquivalence = (proj₂ R) }

and the quotient algebra, in Setoid.Congruences.Basic, is four lines:

  _╱_ : (𝑨 : Algebra {𝑆 = 𝑆} α ρ) → Con 𝑨 ℓ → Algebra α ℓ
  (𝑨 ╱ θ) .Domain = 𝕌[ 𝑨 ] / (Eqv (proj₂ θ))
  (𝑨 ╱ θ) .Interp ⟨$⟩ (f , a) = (f ^ 𝑨) a
  (𝑨 ╱ θ) .Interp .cong {f , u} {.f , v} (refl , a) = is-compatible (proj₂ θ) f a

Read the type first: Algebra α ρ in, Algebra α ℓ out. The carrier level α does not move, because the carrier does not move. Only the level of the equality changes, to the level of the congruence.

Now read the third line. The interpretation of f in the quotient is (f ^ 𝑨) a, which is the interpretation of f in the original algebra, applied to the same arguments. Nothing is chosen, nothing is transported, no representative is picked, because there are no classes to pick from.

The whole content of the construction is the fourth line, the proof that the operations respect the new equality, and that proof is the congruence's own is-compatible field applied to the operation symbol. Compatibility of θ with the operations is the congruence proof the quotient algebra needs. They are not two facts that happen to coincide; they are one fact, stated once, and the setoid formulation is what provides it when needed instead of requiring an extra proof.

Two consequences worth stealing

The canonical projection is the identity function. Here it is, the epimorphism from 𝑨 onto 𝑨 ╱ θ, from Setoid.Homomorphisms.Kernels:

    p : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑨 ╱ θ ]
    p ⟨$⟩ x = x
    p .cong = reflexive (θ .proj₂)

A map between setoids is a function with a proof that it preserves the equalities. The function is id, because the two carriers are the same type. The proof is the reflexive field of the congruence, which asserts that every ≈-equal pair is θ-related.

That field is the part I would have forgotten to include if I had designed IsCongruence from the definition in a textbook, where a congruence is an equivalence relation compatible with the operations and nothing is said about any prior equality. Requiring it looks like pedantry right up until you write this projection, and then it turns out to be exactly what you need: without it the identity function is not a map of setoids, and the reason it is needed is the reason it is true. A congruence has to be an equivalence relation on the setoid rather than on the bare carrier, or the quotient could split an equality class and not be well defined at all.

Proofs about the projection collapse. The kernel of the projection onto 𝑨 ╱ θ is contained in θ, which is a small lemma every development needs. Here is the whole proof:

  ker-in-con : {θ : Con 𝑨 ℓ} → ∀ {x}{y} → kercon (πhom θ) .proj₁ x y →  θ .proj₁ x y
  ker-in-con = id

Two elements are related by the kernel of the projection when their images are θ-related, and their images are themselves! So the two statements are the same, and the proof is the identity function. Here, the elimination rule which goes from equality of two classes back to the relation (and which the frozen Legacy tree calls "cheating") is the reflexive field applied to its argument.

Where the cost reappears

The cost does not disappear; it moves, and it moves somewhere better. The price is paid once per algebra rather than once per theorem.

Building a concrete algebra now means supplying, for each operation, a proof that it respects the equivalence. Setoid.Algebras.Basic has a builder that removes the boilerplate of taking apart the encoding, and is careful to say what the builder does not do.

  mkAlgebra :
    (f : (o : OperationSymbolsOf 𝑆) → Op (ArityOf 𝑆 o) D)
    → (∀ o  → {u v : ArityOf 𝑆 o → D} → (∀ i → u i ≈ v i) → f o u ≈ f o v)
    → Algebra {𝑆 = 𝑆} α ρ

The second argument (the (∀ o ... f o u ≈ f o v) term) is the mathematical content, and it is worth saying precisely why it cannot be derived, because the tempting explanation is wrong.

Function extensionality is a statement about propositional equality: pointwise ≡ gives you ≡ of the two functions. The hypothesis here is pointwise ≈, an (arbitrary) equivalence that we gave the setoid, and no amount of extensionality turns that into f o u ≈ f o v. There is nothing to derive it from: that an operation respects the equivalence is a fact about that operation, and supplying it for each operation is how we turn a carrier into an algebra.

The extensionality remark does fit the other builder. mkAlgebraₚ specializes the carrier to propositional equality, and its obligation reads (∀ i → u i ≡ v i) → f o u ≡ f o v, which is exactly function extensionality followed by cong; it's unavailable here, on purpose. So the general case needs the proof because there is no theorem to reach for, and the propositional case needs it because the theorem is one the library will not assume. Either way every concrete algebra carries a small proof per operation, and the builder only spares you the plumbing around it.

The other cost is felt on every line of every proof. Propositional equality comes with rewrite and subst; a setoid equality comes with neither. Two things being ≈-equal does not let you replace one by the other in a goal, so every step that would have been a rewrite becomes an explicit appeal to the cong, and proofs are written as chains of equational reasoning. The price is more more typing; the reward is mathematics that computes.

The rule and the cubical path

As a rule, if a development is going to take quotients, make equality a parameter of the structure rather than a property of the type. Pay for it where objects are built, which is once, instead of where theorems are proved, which is forever.

That is the argument from cost. The second argument showed up later and I did not plan it: a definition that mentions only the algebra's own equivalence, and never propositional equality, says nothing about what that equivalence is, so porting it to cubical Agda, where the equivalence becomes a path type, is mechanical rather than a redesign. The setoid tree is a step on the way to a cubical one rather than a detour; the frozen tree, whose quotients are built out of blocks and predicates and _≡_, is not.

Every snippet above is verbatim from ualib/agda-algebras at master, commit 4662373d.