[Agda] Postulated computing quotients are unsound

[Nils Anders Danielsson]

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:

     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.

-- 
/NAD