[Agda] Without-K puzzle

[Ulf Norell]

Oh, never mind. Saw Jesper's reply now. Thanks :).

/ Ulf


On Tue, Jul 15, 2014 at 12:47 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

>
> 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/33cf834d/attachment.html