[Agda] Without-K puzzle

[Vladimir Voevodsky]

For puzzle to be provable you need an additional assumption that A is an hSet. This would follow fro example if you new that A has decidable equality. So if decidable equality on Sigma-types is what you are after then it should be provable.

However the step (A has decidable equality) => (A is an hSet)

may be somewhat involved.

V.


On 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/ac335736/attachment.html