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

[James Chapman]

Hi,

On Tue, Feb 15, 2011 at 8:33 PM, Permjacov Evgeniy <permeakra at gmail.com> wrote:
> While I read a thread about ext, what you can suggest to read about
> setoids, assuming that I have not extensive mathematical background?

There is this paper: Setoids in type theory:  Gilles Barthe Venanzio
Capretta and Olivier Pons. In Journal of Functional Programming,
13(2), pages 261-293, 2003
http://www.cs.nott.ac.uk/~vxc/publications/Setoids_JFP_2003.pdf

There are several things by Erik Palmgren too:

Remarks on the relation between families of setoids and identity in
type theory, Institut Mittag-Leffler report 36, 2009/2010
http://www.mittag-leffler.se/preprints/files/IML-0910f-36.pdf
Constructivist and structuralist foundations: Bishop's and Lawvere's
theories of sets, Institut Mittag-Leffler report 4, 2009/2010, fall.
Revised version. http://www2.math.uu.se/~palmgren/cetcs-submit.pdf

Certainly these sound relevant but I think there should be something
else too. Perhaps someone else knows better.
> 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.

If you're interesting in seeing the (dirty!) 'postulate
extensionality' approach in action then you might want to look our
(draft) paper:

Relative monads formalised - Thorsten Altenkirch, James Chapman and
Tarmo Uustalu
the paper can be found here: http://ioc.ee/~james/Publications.html
and a couple of version of the formalisation in Agda can be found
here: http://ioc.ee/~james/relmon.html

Here we used this approach to define and prove properties of some
basic category theory and to prove properties of some programs and
programming related structures. For these purposes this approach seems
to be quite pleasant in my opinion. One helpful use of proof
irrelevance here is if one defines, say, a functor to be the
operations on objects and maps together with the functor laws then
when you need to prove that two functors are equal you need only prove
that the operations are equal.

Cheers,

James