[Agda] Tips for working around proof relevance

[Nicolai Kraus]

On Wed, Dec 16, 2020 at 7:44 PM Thorsten Altenkirch <
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> 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> 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
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201219/f5b7d5c5/attachment.html>