<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's no wonder you didn'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' : ∀ {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' 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'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"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</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>I'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>