# [Agda] Postulated computing quotients are unsound

Benja Fallenstein benja.fallenstein at gmail.com
Wed May 16 16:57:13 CEST 2012

```Hi Nils and all!

I may very well be missing something very obvious, but can you still
make a variant of this go through if instead of

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

you use the following?

private
data Unit : Set where
unit : Unit

Quotient : ∀ {c ℓ} → (A : Setoid c ℓ) → Set (c ⊔ ℓ)
Quotient A = Lift (Unit → Setoid.Carrier A)

The direct translation of your code, included below, unsurprisingly
does not typecheck; the error is:

Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the inferred
indices
[lift (λ _ → true)]
with the expected indices
[lift (λ _ → false)]
when checking that lift (λ _ → true) ≡ lift (λ _ → false) has no
constructors

Cheers,
- Benja

open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])

module Quotient where
private
data Unit : Set where
unit : Unit

Quotient : ∀ {c ℓ} → (A : Setoid c ℓ) → Set (c ⊔ ℓ)
Quotient A = Lift (Unit → Setoid.Carrier A)

[_] : ∀ {c ℓ A} → Setoid.Carrier {c} {ℓ} A → Quotient {c} {ℓ} A
[ x ] = lift (\_ → x)

elim : ∀ {c ℓ r A} → {R : Set r} → let open Setoid {c} {ℓ} A
in (f : Carrier → R)
→ ((x y : Carrier) → x ≈ y → f x ≡ f y)
→ Quotient A → R
elim f q (lift x) = f (x unit)

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

open Quotient using (Quotient; [_]; elim; [_]-cong)

data ⊥ : Set where

record ⊤ : Set where
constructor <>

data Bool : Set where
true false : Bool

myA : Setoid zero zero
myA = record
{ Carrier = Bool
; _≈_ = \_ _ → ⊤
}

p : [_] {A = myA} true ≡ [ false ]
p = [ _ ]-cong