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

[Andreas Abel]

Maybe someone else has a suggestion for literature...

In short, a setoid is a tuple of a type A and a relation R : A -> A -> 
Set which is an equivalence (reflexive, transitive, symmetric).  For 
data types, you can take Leibniz equality as this R, for function types 
A -> B you would define equality extensionally from the equalities R_A 
and R_B:

   R_{A->B} f1 f2 = forall x1 x2, R_A x1 x2 -> R_B (f1 x1) (f2 x2)

R_{A u+ B} y1 y2 would be defined inductively by two constructors

   inj1 : R_A x1 x2 -> R_{A u+ B} (inj1 x1) (inj1 x2)
   inj2 : R_B x1 x2 -> R_{A u+ B} (inj2 x1) (inj2 x2)

Then you can for instance show that

   R_{A u+ B -> A u+ B} (sum inj1 inj2) id

because now you can uses case over the possible arguments x : A u+ B.

Cheers,
Andreas

On 2/15/11 7:33 PM, Permjacov Evgeniy wrote:
> 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
>>>
>>
>
> _______________________________________________
> 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/