[Agda] Postulated computing quotients are unsound

[Dan Licata]

Sorry, my hastily written code fragments were not the right rendering of
"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."  The abstract type 'I' itself clearly needs to have its defintion
hidden, to prevent your counterexample, and I forgot to make it a
one-constructor datatype.

Try this version? :)

-Dan

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

      data I'' : Set where
        mkI'' : (I' × (Unit -> Unit)) -> I''

    I : Set
    I = I''

    zero : I
    zero = mkI'' (Zero , _)
    
    one : I
    one = mkI'' (One , _)

    postulate
      seg : zero ≃ one

    I-rec : {C : Set} 
           -> (a b : C)
           -> (p : a ≃ b)
           -> I -> C
    I-rec a b _ (mkI'' (Zero , _)) = a
    I-rec a b _ (mkI'' (One , _)) = b

    I-elim : {C : I -> Set} 
           -> (a : C zero) (b : C one) (p : subst C seg a ≃ b)
           -> (x : I) -> C x
    I-elim a b _ (mkI'' (Zero , _)) = a
    I-elim a b _ (mkI'' (One , _)) = b

On May16, Dan Doel wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda