# [Agda] Postulated computing quotients are unsound

Dan Licata drl at cs.cmu.edu
Wed May 16 17:38:16 CEST 2012

```Ooh, good idea!  I had trouble getting the dependent elimination rule
for the interval to go through for this kind of definition, though (I
tried with just Unit -> X -- I don't see why you need the lift?).
Essentially the problem is that you need to know (definitionally) that
every term of type Unit -> Bool is \_.true or \_.false.  (Which you
could prove using function extensionality).

However, your idea did suggest the following hack(^2) to me: if you want an
abstract type that doesn't allow absurd patterns, define it to be
whatever you would have defined it to be, paired with Unit -> Unit.

For the interval I (a higher inductive type that comes up in homotopy
type theory, which is essentially booleans "quotiented" by zero = one.
This sounds trivial, but it's useful in higher-dimensional settings):

private
data I' : Set where
Zero : I'
One  : I'

I : Set
I = I' × (Unit -> Unit)

All of the definitons go through, because Unit -> Unit is definitionally
trivial, but the presence of the function blocks the absurd pattern:

oops : Id zero one -> Void
oops ()

gives

The following indices are not constructors (or literals) applied to
variables:
.lib.spaces.Interval.IntervalFn.I'.Zero , (λ _ → <>)
.lib.spaces.Interval.IntervalFn.I'.One , (λ _ → <>)
when checking that the clause oops () has type Id zero one → Void

I realize this is piling a hack on top of a hack, but can anyone break
it?

-Dan

On May16, Benja Fallenstein wrote:
> 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
>
```