[Agda] Tips for working around proof relevance

[Thorsten Altenkirch]

It is something else because you can still observe the codes underlying the setoid and you can define functions that do not repsect the steoid equality.

Setoids are ok once we hide them by making the mandatory. Mixing setoids and sets is harmful.

Thorsten

From: Agda <agda-bounces at lists.chalmers.se> on behalf of Peter LeFanu Lumsdaine <p.l.lumsdaine at gmail.com>
Date: Wednesday, 16 December 2020 at 16:22
To: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>
Cc: "agda at lists.chalmers.se" <agda at lists.chalmers.se>
Subject: Re: [Agda] Tips for working around proof relevance

On Wed, Dec 16, 2020 at 1:40 PM Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk<mailto:Thorsten.Altenkirch at nottingham.ac.uk>> wrote:
>
> But this is not the arrow category it is something else.

No, that construction really is the arrow category (when one is taking “category” = “category with hom-setoids”), and behaves in all the ways you expect the construction to behave!  It’s not “forgetting” the setoid-equalities on arrows — those are still there, just as isomorphisms in the category — so it doesn’t mean you need to make objects a setoid as well, or anything like that.

Following the HoTT/univalent analysis of category theory, one can see that setoid-based categories fit very naturally into the hierarchy of notions of “(n-)category” with varying levels of “saturation”.  Just like “precategories” (e.g. categories in classical foundations) don’t assume saturation/univalence at the object level, if you relax saturation at the levels of arrows/equalities as well, then you get categories with hom-setoids.

I gave the main details of this in my talk at the memorial conference for Erik Palmgren.
Slides: http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf
Video: https://youtu.be/glC8tC7xdBY

Category theory seems to develop well as long as your saturation assumption is of the form “saturated in levels ≥n” for some n.  “Univalent categories” = “saturated in levels ≥0”; “precategories“ = “saturated in levels ≥1”; “setoid-categories” = “not saturated at all” — all of these give a good development of category theory.  “Wild categories” are badly behaved exactly because when you view them in this analysis, they assume “saturation of arrows” (1-saturation) but NOT “saturation of 2-cells” (2-saturation, which turns out to be the condition that equality on arrows is propositional).

There are certainly reasons (theoretical and practical) to prefer the non-setoid versions for many purposes — just as there are purposes for which the setoid versions are good — and also just like how there are advantages and disadvantages to always requiring saturation at the object level.  But these are all natural parts of the same mathematical picture — it certainly isn’t a matter of “the right mathematical way” vs “nasty hacks” or “assembly language”.

–Peter.





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201216/fd65d53d/attachment.html>