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

Matthieu Sozeau matthieu.sozeau at gmail.com
Fri Jan 17 15:18:53 CET 2014


Hi,

  According to a discussion with Dan Licata and Peter Lumsdaine, the problem
is that eliminating refl ≡ refl is not ok (the type of i in test after the first
split), it’s an instance of K. Linking to the other thread on injectivity for cons:

  cons is injective for lists, but that doesn’t hold for all constructors when
you have HITs.

data Foo where
  c1 : Nat → Bool → Foo
  c2 : (a b : Nat) (b : Bool) → c1 a b ≡ c1 (succ a) b

In other words, the no confusion property, constructors are injective and
disjoint and there’s only one equality between them is no longer always 
true… Interestingly, there is existing machinery for per-type, custom 
NoConfusion in the eliminating dependent pattern-matching paper. One more 
argument for going down to eliminators.

Cheers,
— Matthieu

On 17 janv. 2014, at 14:58, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> Thanks for clarifying.
> 
> We are also not relieved, probably... ;-)
> 
> What does your own version of --without-K say?
> 
> Cheers,
> Andreas
> 
> On 17.01.2014 14:43, Jesper Cockx 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
>> <mailto: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>
>>        <mailto: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 <mailto:Agda at lists.chalmers.se>
>>        https://lists.chalmers.se/__mailman/listinfo/agda
>>        <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 <mailto:andreas.abel at ifi.lmu.de>
>>    http://www2.tcs.ifi.lmu.de/~__abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>> 
>> 
> 
> 
> -- 
> 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



More information about the Agda mailing list