[Agda] Postulated computing quotients are unsound

[Dan Doel]

module Quot where

open import Function

open import Data.Empty
open import Data.Unit
open import Data.Product

open import Relation.Binary.PropositionalEquality

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

  I : Set
  I = I' × (Unit → Unit)

  zero : I
  zero = Zero , id

  one : I
  one = One , id

  postulate
    path : zero ≡ one

module Broken where
  open Interval

  bad : ⊥
  bad with cong proj₁ path
  ... | ()

On Wed, May 16, 2012 at 11:38 AM, Dan Licata <drl at cs.cmu.edu> wrote:
> 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
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda