[Agda] Yet another questions about equality

[Dominique Devriese]

Permjacov,

2011/2/15 Permjacov Evgeniy <permeakra at gmail.com>:
> On 02/15/2011 07:25 PM, Andreas Abel wrote:
>
>>> 2) is it possible to prove
>>>    ∀ {ℓ : Level} {A B : Set ℓ} {f g : A → B} → (∀ (a : A) → f a ≡ g a) →
>>> f ≡ g
>>
>>
>> This is functional extensionality, which is not provable in Agda.
> What problem I will face if I postulate this proposition ?

This is a common question on this list. I know because I asked it here
myself a couple of months ago ;). See
http://comments.gmane.org/gmane.comp.lang.agda/2342. In that
discussion, Thorsten Altenkirch also discusses the downside of
postulating ext (no more canonicity). Practically, the problem (as I
understand it) is that you cannot pattern match on an equality proof
constructed using ext.

Dominique