[Agda] Postulated computing quotients are unsound

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


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


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:

     [_]-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

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

* 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

* 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:

     bad : ⊥
     bad with p
     ... | ()

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.


More information about the Agda mailing list