<div dir="ltr"><div><div><span style="font-family:arial,helvetica,sans-serif">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.<br>
<br></span></div><span style="font-family:arial,helvetica,sans-serif">Best,<br></span></div><span style="font-family:courier new,monospace"><span style="font-family:arial,helvetica,sans-serif">Jesper</span><br></span></div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jan 17, 2014 at 12:19 PM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><div><div><div><div><div>Dear all,<br><br></div>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?<br>
<br></div>=== BEGIN CODE ===<br><br><span style="font-family:courier new,monospace">{-# OPTIONS --without-K #-}<br><br>module YetAnotherWithoutKProblem where<br><br>-- First, some preliminaries to make this file self-contained.<br>
data _≡_ {a} {A : Set a} (x : A) : A → Set where<br> refl : x ≡ x<br><br>subst : ∀ {a b} {A : Set a} {x : A} (B : (y : A) → Set b) →<br> {y : A} → x ≡ y → B x → B y<br>subst B refl b = b<br><br>record _≃_ (A B : Set) : Set where<br>
constructor equiv<br> field<br> f : A → B<br> g : B → A<br> i : (x : A) → g (f x) ≡ x<br> j : (y : B) → f (g y) ≡ y<br><br>-- The univalence axiom.<br>postulate equiv-to-id : {A B : Set} → A ≃ B → A ≡ B<br>
<br>-- Now consider any concrete space 'mySpace' with a point 'myPoint'.<br>-- We will show that mySpace has no structure above dimension 2.<br>postulate mySpace : Set<br>postulate myPoint : mySpace<br><br>
-- We define Foo in a way such that 'Foo e' is equivalent with 'refl ≡ e'.<br>data Foo : myPoint ≡ myPoint → Set where<br> foo : Foo refl<br><br>Foo-equiv : {e : myPoint ≡ myPoint} → Foo e ≃ (refl ≡ e)<br>
Foo-equiv = equiv f g i j <br> where<br> f : {e : myPoint ≡ myPoint} → Foo e → refl ≡ e<br> f foo = refl<br><br> g : {e : myPoint ≡ myPoint} → refl ≡ e → Foo e<br> g refl = foo<br><br> i : {e : myPoint ≡ myPoint} (m : Foo e) → g (f m) ≡ m<br>
i foo = refl<br><br> j : {e : myPoint ≡ myPoint} (i : refl ≡ e) → f (g i) ≡ i<br> j refl = refl<br><br>-- Here comes the real problem: by injectivity, 'Foo e' is a set ...<br>test : {e : myPoint ≡ myPoint} → (a : Foo e) → (i : a ≡ a) → i ≡ refl<br>
test foo refl = refl<br><br>-- ... hence by univalence, so is 'refl ≡ e'.<br>problem : {e : myPoint ≡ myPoint} → (a : refl ≡ e) → (i : a ≡ a) → i ≡ refl<br>problem = subst (λ X → (x : X) → (i : x ≡ x) → i ≡ refl) <br>
(equiv-to-id Foo-equiv) <br> test</span><br><br></div>=== END CODE ===<br><br></div>All the best,<br></div>Jesper<br></div>
</blockquote></div><br></div>