[Agda] Yet another questions about equality

[Permjacov Evgeniy]

On 02/16/2011 03:17 PM, Thorsten Altenkirch wrote:
> 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). 
And how it should work, If I want endo-mapping ? specifically, how I can
formulate and prove, that
fot   [code] upcast f = sum inj\_1 ( \x -> inj\_2 (f x) )  [/code] 
holds   [code] upcast id `equal` id [/code]?

> 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).
>
What is wrong with structural inductive definition, i. e. defining basic
types like (sum A B) (A * B) () and so on and defining  a \== a and
several 'lifting' type constructors (such as (f `eq` g -> a -> f a `eq f
g) and vice versa) ? Definitly, it should be quite ugly and may require
some form of reflection and may not work for highter universes, yet...
what the problem?
 
> Cheers,
> Thorsten