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

[Andreas Abel]

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.

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
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/