[Agda] Tips for working around proof relevance

[Thorsten Altenkirch]

I rather think that is a clever defense of a bad idea. Setoids are the workaround for a lack of extensionality the sooner people stop using them the better.

Sent from my iPhone

On 19 Dec 2020, at 21:47, Nicolai Kraus <nicolai.kraus at gmail.com> wrote:


On Wed, Dec 16, 2020 at 7:44 PM Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk<mailto:Thorsten.Altenkirch at nottingham.ac.uk>> wrote:
It is something else because you can still observe the codes underlying the setoid

I think you say this because you view setoid-categories as a hack to make the implementation work. Something can be a hack and, by coincidence (?), a mathematically meaningful concept at the same time. For me, Peter's email/talk explains why this is the case here. It's really not surprising that there are different views: If you have a bicategory, the 2-morphisms could be exposing implementation details (which you want to hide), but they could also be interesting structure (which you want to see). One really has to judge on a case-by-case basis.

and you can define functions that do not repsect the steoid equality.

Functors have to preserve the setoid morphisms. It's part of the structure, in the same way as it's part of the structure that functors act on the category morphisms. Sure, it's not automatic in the sense it is automatic for >=1-saturated/completed categories.

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

I don't think "harmful" is the right word here... As Peter has explained, the "mix" gives you a notion of "unsaturated category", and this notion turns out to be well-behaved.

Nicolai


Thorsten

From: Agda <agda-bounces at lists.chalmers.se<mailto:agda-bounces at lists.chalmers.se>> on behalf of Peter LeFanu Lumsdaine <p.l.lumsdaine at gmail.com<mailto:p.l.lumsdaine at gmail.com>>
Date: Wednesday, 16 December 2020 at 16:22
To: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk<mailto:psztxa at exmail.nottingham.ac.uk>>
Cc: "agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>" <agda at lists.chalmers.se<mailto: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.





_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda



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/20201220/dfbbfa7e/attachment.html>