<div dir="ltr">I'm not relieved. The problem is still there.<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jan 17, 2014 at 2:38 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Can you explain, please?<br>
<br>
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?<br>
<br>
Sorry, I am a bit confused now...<br>
Andreas<div class="im"><br>
<br>
On 17.01.2014 13:39, Jesper Cockx wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
As Martin pointed out to me, my definition of equiv-to-id is not the<br>
univalence axiom, but merely a (much weaker) consequence of it. Thank you.<br>
<br>
Best,<br>
Jesper<br>
<br>
<br>
On Fri, Jan 17, 2014 at 12:19 PM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a><br></div><div><div class="h5">
<mailto:<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>>> wrote:<br>
<br>
Dear all,<br>
<br>
Much to my own surprise, I encountered another problem with the<br>
--without-K option. This is on the latest darcs version of Agda and<br>
is unrelated to the termination checker. As far as I understand, the<br>
unification algorithm is applying the injectivity rule too liberally<br>
for data types indexed over indexed data. But maybe someone else can<br>
give a better explanation?<br>
<br>
=== BEGIN CODE ===<br>
<br>
{-# 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<br>
≡ 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<br>
≡ refl<br>
problem = subst (λ X → (x : X) → (i : x ≡ x) → i ≡ refl)<br>
(equiv-to-id Foo-equiv)<br>
test<br>
<br>
=== END CODE ===<br>
<br>
All the best,<br>
Jesper<br>
<br>
<br>
<br>
<br></div></div><div class="im">
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
</div></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br></div>