The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

Hi Russell,

Olov Wilander shows that PERs, unlike setoids, have *given* pullbacks.
That is, pullbacks respect equalities.
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-159876

In fact, all the basic constructions are given. This may be related to
what you are suggesting?

Best,

Bas

On Thu, Nov 10, 2011 at 5:47 PM,  
<roconnor AT theorem.ca>
 wrote:
> On Wed, 9 Nov 2011, Carlos Simpson wrote:
>
>> Dear Russell,
>>  Thanks, that's illuminating. I guess the question which can make us
>> uneasy about using setoids, is whether it causes too much extra effort to
>> prove that all functions are compatible all the time? That kind of fear
>> does
>> sometimes prove to be overblown.
>
> The amount of work needed to prove that functions are respectful is exactly
> the amount of work needed to show that a function is well-defined using
> quotients (ie the work needed to satisfy the hypothesis of
> ZornsLemma.Quotients.induced_fuction).  Then some sort of type-class
> mechanism needs to take over to prove that compositions of respectful
> functions are respectful.
>
>> One imagines that all of the CIC operations we can do on types, need to be
>> done by hand for setoids. Is it the case that you actually end up having
>> only a small number of these to do in practice? ---Carlos
>
> There is something to this point.  You need need to write a library to make
> products of setoid, and disjoint unions of setoids, and setoid function
> spaces (*).  However, I never really had a problem with this because we have
> to do this sort of thing all the time anyways.  So, for example, when doing
> my work on metric spaces I needed to define a metric for the product of two
> metric spaces, and a metric for functions between metric spaces, etc.  Since
> I had to all this work anyways, I didn't find it particularly burdensome to
> define these operations on setoids while I was at it.
>
> (*) Actually I did discover some annoyance with setoids and function spaces.
>  You need to put a setoid structure on a sigma-type of functions that are
> respectful.  What I discovered was that everything would probably be better
> if PERs were used instead of setoids.  The PER of functions between Setoids
> is exactly what you expect:
>
> f ~~ g := forall x y, x == y -> f x == g y
>
> And we immediately get that a function f is respectful when f ~~ f.  And
> this definition extends to the PER of functions between PERs
>
> f ~~ g := forall x y, x ~~ y -> f x ~~ g y
>
> I spent a while slogging through this PER stuff and every obstacle I
> encountered eventually yielded to an elegant solution.  I suspect that the
> experts on PERs already knew all this stuff I was discovering. Unfortunately
> at the time (several years ago) I couldn't quite get the support out of
> Mathieu's type class mechanism that I needed to make this seamless.  I
> suspect it would be easier today or one could use Canonical Structures
> instead. I would encourage the development and use of PERs instead of
> setoids.
>
> --
> Russell O'Connor                                      <http://r6.ca/>
> ``All talk about `theft,''' the general counsel of the American Graphophone
> Company wrote, ``is the merest claptrap, for there exists no property in
> ideas musical, literary or artistic, except as defined by statute.''
>