[Agda] Without-K puzzle

[Martin Escardo]

On 15/07/14 16:27, Vladimir Voevodsky wrote:
> 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.

Ulf,

There is a proof in Agda here that you can reuse:
http://www.cs.bham.ac.uk/~mhe/GeneralizedHedberg/html/GeneralizedHedberg.html#4865

Martin

>
> V.
>
>
> On Jul 15, 2014, at 11:07 AM, Ulf Norell <ulf.norell at gmail.com
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe