<div dir="ltr"><div><div><div>The type of <font face="courier new, monospace">puzzle is actually the contrapositive of the principle of equality of second projections, which is equivalent with K. So it&#39;s no wonder you didn&#39;t manage to prove it. At least the level-generic version of puzzle is inconsistent with univalence:<br>

<br><br>data Bool : Set where true false : Bool<br><br>true≠false : ¬ Id Bool true false<br>true≠false ()<br><br>no-univalence : ¬ Id _ (Bool , true) (Bool , false)<br>no-univalence = puzzle Set (λ X → X) Bool true false true≠false<br>

<br><br></font></div><font face="courier new, monospace">However, puzzle should be provable in case you know that the type A has decidable equality. To start with, it may help to prove a generalized version of puzzle:<br>

<br><br>transport : ∀ {a p} {A : Set a} (P : A → Set p) →<br>            {x y : A} → Id A x y → P x → P y<br>transport P refl p = p<br><br>puzzle&#39; : ∀ {a b} (A : Set a) (B : A → Set b) (x₁ x₂ : A) (y : B x₁) (z : B x₂) →<br>

          (p : Id A x₁ x₂) → ¬ Id (B x₂) (transport B p y) z → ¬ Id (Σ A B) (x₁ , y) (x₂ , z)<br>puzzle&#39; A B x₁ .x₁ y .y p neq refl = {!!}<br><br><br></font></div><font face="courier new, monospace">Now, neq has type [¬ Id (B x₁) (transport B p y) y], so the problem is now to prove that [transport B p y] equals y. If A has decidable equality, then it satisfies UIP by Hedberg&#39;s theorem, hence p must equal refl and [transport B p y] equals y. I hope this helps.<br>

<br></font></div><font face="courier new, monospace">Jesper<br></font><div><div><div><font face="courier new, monospace"><br></font></div></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jul 15, 2014 at 11:07 AM, Ulf Norell <span dir="ltr">&lt;<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>&gt;</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>I&#39;ve been trying to define decidable equality on sigma types without K and I run into<br></div>

<div>problems in the case where the first components are equal but the second ones are<br></div><div>not. It boils down to solving the puzzle below, proving the contra-positive of injectivity<br>

</div><div>of _,_ in the second argument. Any without-K wizard that can give me a hand with this?<br></div><br><div><div><font face="courier new, monospace">data ⊥ : Set where</font></div><div><font face="courier new, monospace"><br>



</font></div><div><font face="courier new, monospace">¬_ : Set → Set</font></div>
<div><font face="courier new, monospace">¬ A = A → ⊥</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">data Σ (A : Set) (B : A → Set) : Set where</font></div><div>




<font face="courier new, monospace">  _,_ : (x : A) → B x → Σ A B</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">data Id (A : Set) (x : A) : A → Set where</font></div>




<div><font face="courier new, monospace">  refl : Id A x x</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">elim-Id : {A : Set} (P : ∀ x y → Id A x y → Set) →</font></div>




<div><font face="courier new, monospace">          (∀ x → P x x refl) →</font></div><div><font face="courier new, monospace">          ∀ x y (p : Id A x y) → P x y p</font></div><div><font face="courier new, monospace">elim-Id P r x .x refl = r x</font></div>




<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">puzzle : (A : Set) (B : A → Set) (x : A) (y z : B x) →</font></div><div><font face="courier new, monospace">         ¬ Id (B x) y z → ¬ Id (Σ A B) (x , y) (x , z)</font></div>




<div><font face="courier new, monospace">puzzle A B x y z neq eq = ?</font></div></div><span class="HOEnZb"><font color="#888888"><div><br></div><div>/ Ulf</div></font></span></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>