[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