[Agda] Tips for working around proof relevance

[Peter LeFanu Lumsdaine]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201216/f3014c07/attachment.html>