[Agda] Without-K puzzle

[Martin Escardo]

But I have the feeling that it should be possible to side-step Hedberg's 
theorem in the proof that if A has decidable equality and B(a) has 
decidable equality for every a:A, then Sigma A B is decidable. But I 
haven't had any free time today (being at VSL) to try this out.

Moreover, it should be possible to show a more general result: if a:A is 
isolated and b:B(a) is isolated, then (a,b) is isolated.

Here I say that an element x:X is isolated if x=y is decidable for every 
y:X. There are types without decidable equality but with isolated 
elements. A trivial one is 1+A for any type A, a less trivial one is 
N+A, and there are even less trivial ones, such as the type of 
decreasing binary sequences, in which the eventually constant zero ones 
are isolated, but the constanly 1 sequence is not. I proved this here

http://www.cs.bham.ac.uk/~mhe/agda/GenericConvergentSequence.html#6217

without using Hedberg, and this type is in fact a Sigma type.

Martin

On 15/07/14 16:42, Martin Escardo wrote:
>
>
> 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