Fwd: Re: [Agda] Yet another questions about equality

[Permjacov Evgeniy]

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 ?


>
> For the same reason, 1) is not provable.
>
> Leibniz equality \equiv is intensional, so functions can be different
> even if they behave the same on all arguments.  [This is not so
> unnatural, e.g., quick sort and insertion sort have the same
> observational behavior, they both sort, but they are still different
> functions.]
>
> Maybe you want extensional equality, this can be done in general using
> setoids.
>
The problem 1) emerged, when I tried to prove, that \all {A : Set \ell}
\->( \lambda B \-> A \u+ ) is a Functor . Specifically,
 sum inj\_1 inj\_2 \== id is proposition, proving that  identity arrow
raised from underling category is identity arrow in target category. I
fear size of standart library, so I'm building my own, more faced to
programming rather than reasoning.