[Agda] Without-K puzzle

[Jesper Cockx]

The type of puzzle is actually the contrapositive of the principle of
equality of second projections, which is equivalent with K. So it's no
wonder you didn't manage to prove it. At least the level-generic version of
puzzle is inconsistent with univalence:


data Bool : Set where true false : Bool

true≠false : ¬ Id Bool true false
true≠false ()

no-univalence : ¬ Id _ (Bool , true) (Bool , false)
no-univalence = puzzle Set (λ X → X) Bool true false true≠false


However, puzzle should be provable in case you know that the type A has
decidable equality. To start with, it may help to prove a generalized
version of puzzle:


transport : ∀ {a p} {A : Set a} (P : A → Set p) →
            {x y : A} → Id A x y → P x → P y
transport P refl p = p

puzzle' : ∀ {a b} (A : Set a) (B : A → Set b) (x₁ x₂ : A) (y : B x₁) (z : B
x₂) →
          (p : Id A x₁ x₂) → ¬ Id (B x₂) (transport B p y) z → ¬ Id (Σ A B)
(x₁ , y) (x₂ , z)
puzzle' A B x₁ .x₁ y .y p neq refl = {!!}


Now, neq has type [¬ Id (B x₁) (transport B p y) y], so the problem is now
to prove that [transport B p y] equals y. If A has decidable equality, then
it satisfies UIP by Hedberg's theorem, hence p must equal refl and
[transport B p y] equals y. I hope this helps.

Jesper



On Tue, Jul 15, 2014 at 11:07 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140715/42a7657d/attachment.html