[Agda] Postulated computing quotients are unsound

[Dan Licata]

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
>