[Agda] Re: Yet another way Agda --without-K is incompatible with
univalence
Jesper Cockx
Jesper at sikanda.be
Fri Jan 17 15:34:31 CET 2014
Andreas: my own version of --without-K has the same problem. However, I'm
trying to fix it by doing something like parameter reconstruction for the
indices: when applying the injectivity rule to the problem "foo ≡ foo", we
should first solve the equation "refl ≡ refl" on the indices (here, both
refl's have type "myPoint ≡ myPoint"). But this equation is already
rejected by the current --without-K, thus excluding the problematic pattern
matching on "foo ≡ foo". I'm still testing whether this doesn't introduce
any other problems or excludes any good examples.
Matteo: the problem with allowing no pattern matching at all is that in
Agda, we depend on pattern matching to define eliminators for data types.
Another possibility would be to introduce an even more restrictive version
of --without-K that requires all indices (and parameters too possibly?) to
be *distinct* variables (so no constructors allowed). This would at least
allow us to define the eliminator for each data type, but hopefully be
simple enough to avoid any problems like this one.
Mattieu: The equation that's being eliminated is "foo ≡ foo", which is
indeed the same as "refl ≡ refl" under the equivalence Foo-equiv. However
unlike refl, the constructor foo has no parameters and no arguments, so a
naive interpretation of injectivity would tell you that the only term of
type "foo ≡ foo" is refl. However, this is ignoring the index of the type
Foo. So in fact, we first need to solve the equation "refl ≡ refl" on the
indices, which is impossible without K.
Best,
Jesper
On Fri, Jan 17, 2014 at 3:02 PM, Matteo Acerbi <matteo.acerbi at gmail.com>wrote:
> Hello,
>
> I noticed that if the two postulates are replaced by
>
> module _ (mySpace : Set)(myPoint : mySpace) where
>
> (indent the rest)
>
> the problem seems to not appear (an error is reported).
>
> Maybe this gives some hints (I do not know).
>
> That said, I have a small proposal.
>
> Most of the times I use Agda for its *wonderful* dependent pattern
> matching facility, but every now and then I would like to forbid
> myself to use pattern matching at all, at least from inside a single
> file.
>
> I would like to have the possibility to get back to that file and make
> sure that I never used pattern matching in that code just by looking
> at the OPTIONS header.
>
> I think I would find a --no-pattern-matching option, which simply
> applied this restriction, but still allowed for importing modules
> whatever their options are, very convenient.
>
> For now I am just curious as to whether others are interested: would
> anyone else like such a --no-pattern-matching option?
>
> Cheers,
> Matteo
>
> On Fri, Jan 17, 2014 at 2:43 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
> > I'm not relieved. The problem is still there.
> >
> >
> > On Fri, Jan 17, 2014 at 2:38 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
> > wrote:
> >>
> >> Can you explain, please?
> >>
> >> You say you did not expect to be able to prove 'problem' from
> >> 'equiv-to-id' which you thought was univalence. Martin tells you that
> >> 'equiv-to-id' is a consequence of univalence. Now you are relieved. But
> >> still 'problem' follows from univalence. Why are you relieved now?
> >>
> >> Sorry, I am a bit confused now...
> >> Andreas
> >>
> >>
> >> On 17.01.2014 13:39, Jesper Cockx wrote:
> >>>
> >>> As Martin pointed out to me, my definition of equiv-to-id is not the
> >>> univalence axiom, but merely a (much weaker) consequence of it. Thank
> >>> you.
> >>>
> >>> Best,
> >>> Jesper
> >>>
> >>>
> >>> On Fri, Jan 17, 2014 at 12:19 PM, Jesper Cockx <Jesper at sikanda.be
> >>> <mailto:Jesper at sikanda.be>> wrote:
> >>>
> >>> Dear all,
> >>>
> >>> Much to my own surprise, I encountered another problem with the
> >>> --without-K option. This is on the latest darcs version of Agda and
> >>> is unrelated to the termination checker. As far as I understand,
> the
> >>> unification algorithm is applying the injectivity rule too
> liberally
> >>> for data types indexed over indexed data. But maybe someone else
> can
> >>> give a better explanation?
> >>>
> >>> === BEGIN CODE ===
> >>>
> >>> {-# OPTIONS --without-K #-}
> >>>
> >>> module YetAnotherWithoutKProblem where
> >>>
> >>> -- First, some preliminaries to make this file self-contained.
> >>> data _≡_ {a} {A : Set a} (x : A) : A → Set where
> >>> refl : x ≡ x
> >>>
> >>> subst : ∀ {a b} {A : Set a} {x : A} (B : (y : A) → Set b) →
> >>> {y : A} → x ≡ y → B x → B y
> >>> subst B refl b = b
> >>>
> >>> record _≃_ (A B : Set) : Set where
> >>> constructor equiv
> >>> field
> >>> f : A → B
> >>> g : B → A
> >>> i : (x : A) → g (f x) ≡ x
> >>> j : (y : B) → f (g y) ≡ y
> >>>
> >>> -- The univalence axiom.
> >>> postulate equiv-to-id : {A B : Set} → A ≃ B → A ≡ B
> >>>
> >>> -- Now consider any concrete space 'mySpace' with a point
> 'myPoint'.
> >>> -- We will show that mySpace has no structure above dimension 2.
> >>> postulate mySpace : Set
> >>> postulate myPoint : mySpace
> >>>
> >>> -- We define Foo in a way such that 'Foo e' is equivalent with
> 'refl
> >>> ≡ e'.
> >>> data Foo : myPoint ≡ myPoint → Set where
> >>> foo : Foo refl
> >>>
> >>> Foo-equiv : {e : myPoint ≡ myPoint} → Foo e ≃ (refl ≡ e)
> >>> Foo-equiv = equiv f g i j
> >>> where
> >>> f : {e : myPoint ≡ myPoint} → Foo e → refl ≡ e
> >>> f foo = refl
> >>>
> >>> g : {e : myPoint ≡ myPoint} → refl ≡ e → Foo e
> >>> g refl = foo
> >>>
> >>> i : {e : myPoint ≡ myPoint} (m : Foo e) → g (f m) ≡ m
> >>> i foo = refl
> >>>
> >>> j : {e : myPoint ≡ myPoint} (i : refl ≡ e) → f (g i) ≡ i
> >>> j refl = refl
> >>>
> >>> -- Here comes the real problem: by injectivity, 'Foo e' is a set
> ...
> >>> test : {e : myPoint ≡ myPoint} → (a : Foo e) → (i : a ≡ a) → i ≡
> refl
> >>> test foo refl = refl
> >>>
> >>> -- ... hence by univalence, so is 'refl ≡ e'.
> >>> problem : {e : myPoint ≡ myPoint} → (a : refl ≡ e) → (i : a ≡ a) →
> i
> >>> ≡ refl
> >>> problem = subst (λ X → (x : X) → (i : x ≡ x) → i ≡ refl)
> >>> (equiv-to-id Foo-equiv)
> >>> test
> >>>
> >>> === END CODE ===
> >>>
> >>> All the best,
> >>> Jesper
> >>>
> >>>
> >>>
> >>>
> >>> _______________________________________________
> >>> Agda mailing list
> >>> Agda at lists.chalmers.se
> >>> https://lists.chalmers.se/mailman/listinfo/agda
> >>>
> >>
> >>
> >> --
> >> Andreas Abel <>< Du bist der geliebte Mensch.
> >>
> >> Theoretical Computer Science, University of Munich
> >> Oettingenstr. 67, D-80538 Munich, GERMANY
> >>
> >> andreas.abel at ifi.lmu.de
> >> http://www2.tcs.ifi.lmu.de/~abel/
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140117/01ecd9c3/attachment-0001.html
More information about the Agda
mailing list