[Agda] Without-K puzzle

[Ulf Norell]

On Tue, Jul 15, 2014 at 11:23 AM, Matthieu Sozeau <mattam at mattam.org> wrote:

>
> I think this is not gonna be provable, as even if y = z is not inhabited,
> tranport p y = z,
> which is the equality you get on the second components, might be. In other
> words, without K you might have transport p y <> y for p : x = x.
> An example is if p : Bool = Bool is the negation iso, B := \x. x, y :=
> true, z := false. So you need to assume A is an HSet here, or is decidable.
>

Ok, that's fair. Fortunately in my case equality on A is decidable (I'm
trying to lift decidable equality on A and B to decidable equality on Σ A B).
How would I use that to prove the puzzle?

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