# [Agda] Postulated computing quotients are unsound

Nils Anders Danielsson nad at chalmers.se
Wed May 16 15:13:57 CEST 2012

```Hi,

At the last AIM Thorsten Altenkirch, James Chapman and I experimented
with postulated, computing quotients, perhaps inspired by Dan Licata's
"Running Circles Around (In) Your Proof Assistant; or, Quotients that
Compute":

http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/

We were not sure if this hack was sound or not. Now, thanks to Dan Doel,
I know that it isn't.

Quotients were defined in the following way:

data Quotient {c ℓ} (A : Setoid c ℓ) : Set (c ⊔ ℓ) where
box : (x : Setoid.Carrier A) → Quotient A

To avoid direct pattern matching we didn't export the constructor, but
only a function [_] = box. We also exported an eliminator that allowed
you to "pattern match" as long as you proved that you respected the
relation, as well as the following postulate, which states that [_]
respects the relation:

postulate
[_]-cong : ∀ {c ℓ} {A : Setoid c ℓ} {a₁ a₂} → let open Setoid A in
a₁ ≈ a₂ → _≡_ {A = Quotient A} [ a₁ ] [ a₂ ]

Dan Doel pointed out [1] that certain hacks intended to emulate "higher
inductive types" (as in Dan Licata's post mentioned above) are
suspicious:

* Even if you hide the constructors the absurd pattern is still
available.

* The exported constructors compute to the real ones, also in
equalities. For instance, [ true ] ≡ [ false ] computes to box true ≡
box false.

Given these observations it is easy to prove that the postulate above is
unsound:

* Quotient Bool by the trivial relation.

* Use [_]-cong to prove that [ true ] and [ false ] are equal. Denote
the proof by p.

* Prove that the empty type is inhabited by using an absurd pattern:

... | ()

A similar approach can be used to prove that Dan Licata's encoding of
the interval is unsound.

[1] The #agda IRC channel, 2012-05-15
(http://agda.orangesquash.org.uk/2012/May/16.html); Dan Doel's nick
is dolio.

--