<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><div><br></div><div>/ Ulf</div></div>