[Agda] dependent extensionality

[Vladimir Voevodsky]

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