[Agda] Yet another questions about equality

[Andreas Abel]

If you are happy to work with a closed set of types, for instance 
0,1,+,*,->, then you can define your own language of types (called a 
universe) and define equality recursively on these types.

data U : Set where
   empty unit : U
   _+_ _*_ _=>_ : U -> U -> U

El : U -> Set
El empty = Empty  -- the real empty type
El unit  = Unit   -- the real unit type
El (a => b) = El a -> El b  -- etc.

Eq : (a : U) -> El a -> El a -> Set
Eq empty () ()
Eq unit  t  t' = Unit
Eq (a => b) f f' = forall x x', Eq a x x' -> Eq b (f x) (f' x')

etc.

Cheers,
Andreas

On 2/16/11 1:43 PM, Permjacov Evgeniy wrote:
> 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
>
> _______________________________________________
> 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/