[Agda] Postulated computing quotients are unsound

[Benja Fallenstein]

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

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