<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">For puzzle to be provable you need an additional assumption that A is an hSet. This would follow fro example if you new that A has decidable equality. So if decidable equality on Sigma-types is what you are after then it should be provable.<div><br></div><div>However the step (A has decidable equality) => (A is an hSet)</div><div><br></div><div>may be somewhat involved.</div><div><br></div><div>V.</div><div><br></div><div><br><div><div>On Jul 15, 2014, at 11:07 AM, Ulf Norell <<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><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><div><br></div><div>/ Ulf</div></div>
_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></blockquote></div><br></div></body></html>