<div dir="ltr">I&#39;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">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</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 &#39;problem&#39; from &#39;equiv-to-id&#39; which you thought was univalence.  Martin tells you that &#39;equiv-to-id&#39; is a consequence of univalence.  Now you are relieved. But still &#39;problem&#39; 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 &lt;<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a><br></div><div><div class="h5">
&lt;mailto:<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>&gt;&gt; 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 &#39;mySpace&#39; with a point &#39;myPoint&#39;.<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 &#39;Foo e&#39; is equivalent with &#39;refl<br>
    ≡ e&#39;.<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, &#39;Foo e&#39; 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 &#39;refl ≡ e&#39;.<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  &lt;&gt;&lt;      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>