[Agda] Without-K puzzle

[Ulf Norell]

I've been trying to define decidable equality on sigma types without K and
I run into
problems in the case where the first components are equal but the second
ones are
not. It boils down to solving the puzzle below, proving the contra-positive
of injectivity
of _,_ in the second argument. Any without-K wizard that can give me a hand
with this?

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (x : A) → B x → Σ A B

data Id (A : Set) (x : A) : A → Set where
  refl : Id A x x

elim-Id : {A : Set} (P : ∀ x y → Id A x y → Set) →
          (∀ x → P x x refl) →
          ∀ x y (p : Id A x y) → P x y p
elim-Id P r x .x refl = r x

puzzle : (A : Set) (B : A → Set) (x : A) (y z : B x) →
         ¬ Id (B x) y z → ¬ Id (Σ A B) (x , y) (x , z)
puzzle A B x y z neq eq = ?

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140715/be8e5518/attachment-0001.html