Fwd: [Agda] Re: Yet another way Agda --without-K is incompatible with univalence

[Matteo Acerbi]

This was meant to reach the list, sorry.

---------- Forwarded message ----------
From: Matteo Acerbi <matteo.acerbi at gmail.com>
Date: Fri, Jan 17, 2014 at 3:02 PM
Subject: Re: [Agda] Re: Yet another way Agda --without-K is
incompatible with univalence
To: Jesper Cockx <Jesper at sikanda.be>


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
>