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

[Permjacov Evgeniy]

On 02/15/2011 09:42 PM, Andreas Abel wrote:
> 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
>
This looks simple. however, there is a problem. Let as assume, that we
defined Setoid for A : Set l . This is not a setoid for F A : Set lI
where F : Set l -> Set lI . So, a some way of 'lifting' equivalence from
one setoid to another, associated with equality lifting, wich lifts
equivalence relation from a 'eq-on-A ' b to  f a 'eq-on-B' f b is
needed. How it can be resolved ?