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

[Permjacov Evgeniy]

On 02/15/2011 09:24 PM, Andreas Abel wrote:

> For pragmatical reasons, I agree with Thorsten that you should proceed
> by postulating functional extensionality and keep your fingers
> crossed.  Setoids are the cleaner solution, but involve a lot of work.
>
While I read a thread about ext, what you can suggest to read about
setoids, assuming that I have not extensive mathematical background?

> Cheers,
> Andreas
>
> On 2/15/11 6:04 PM, Permjacov Evgeniy wrote:
>> 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.
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>