[Agda] dependent extensionality

[Thorsten Altenkirch]

This was my suspicion. Can you sketch some details of the construction?

Cheers,
Thorsten

On 29 Sep 2010, at 18:36, Vladimir Voevodsky wrote:

> I am not a specialist in Agda, but I think that I know of a model of the Coq system (modulo the nasty business of "singleton elimination")  which shows that the equality of the maps f1, f2: A -> \sum a:A. B obtained from the  s1, s2: \prod a:A, B does not imply the equality of the sections. The model is incompatible with K. 
> 
> Vladimir.
> 
> 
> 
> 
> 
> 
> On Sep 29, 2010, at 1:32 PM, Conor McBride wrote:
> 
>> Hi James
>> 
>> Homogeneous it may be, but...
>> 
>> On 29 Sep 2010, at 17:58, James Chapman wrote:
>> 
>>> I accidentally chopped the theorem off the bottom. Here's (hopefully)
>>> a more successful cut and paste...
>>> 
>>> substlem : {A : Set}(P : A → Set){a a' : A}(p : a ≡ a')(x : P a)(q : P
>>> a ≡ P a') → subst (λ x → x) q x ≡ subst P p x
>>> substlem P refl x refl = refl
>> 
>> ...here be K        ^^^^
>> 
>> Funny business
>> 
>> Conor
>> 
>> 
>> _______________________________________________
>> Agda mailing list
>> 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