[Agda] Yet another questions about equality

[Thorsten Altenkirch]

On 16 Feb 2011, at 05:38, Permjacov Evgeniy wrote:

> 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 ?

Good point.

Operations on Sets have to be lifted to operations on setoids, i.e. you need to define F* : Setoid -> Setoid. The original F can by projecting the carrier out of F* (\Nabla A) where \Nabla A is the trivial embedding Set -> Setoid (using propositional equality). 

Btw, I completely agree with Peter Hancock that we should use/look for a computational sound interpretation of ext (such as OTT). However, OTT and my earlier LICS paper rely on proof irrelevance which is incompatible with the recent developments related to univalent foundations (which is basically a strengthening of ext by considering an extensional equality of sets called weak equivalence).

Cheers,
Thorsten