<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
Peter, thanks a lot for explaining this [again]! It's a really
interesting observation that setoid-categories are a "maximally
unsaturated" version of 1-categories. <br>
<br>
What is unfortunate is that such unsaturated notions are very
representation-dependent. Different choices of representation, which
would lead to equivalent saturated definitions, give non-equivalent
unsaturated definitions. Do you have intuition for which choices
lead to well-behaved structures? Or is this just a matter of trying
it out?<br>
<br>
My impression is that, in order to get well-behaved structures, we
either want no redundancy at all *or* as much redundancy, and thus
"leeway", as possible. Here, I mean "redundancy" in the sense of
"missing conditions on which components should be identified".
Intuition: If we do a construction and all the input is perfect,
then we hopefully can expect the result to be perfect, so the
construction works. Or, if the input doesn't satisfy any conditions,
but we also don't require the output to satisfy any conditions, then
the construction also works. But if the input is "partially ok" and
the output is required to be "partially ok", then the risk is that
the wrong part of the output will be "partially ok". This is similar
to what you said about saturation (and probably something similar
can be said about strictness).<br>
<br>
Univalent categories have no redundancy, and the agda-categories
library includes a lot of redundancy. What if we remove some
redundancy from agda-categories? If, for example, we remove
`sym-assoc` in<br>
<a class="moz-txt-link-freetext" href="https://agda.github.io/agda-categories/Categories.Category.Core.html">https://agda.github.io/agda-categories/Categories.Category.Core.html</a><br>
and replace all occurrences by what we get from `assoc` and the
witness of `IsEquivalence (_≈_)`? This would cause more work in some
places (judging by the comment on why `sym-assoc` was included), but
could all constructions still be fixed? I would expect they can, but
I don't think it's a priori clear. Jacques, did you find that some
redundancy is really required rather than just convenient in the
implementation?<br>
<br>
Nicolai<br>
<br>
<br>
<div class="moz-cite-prefix">On 16/12/2020 16:20, Peter LeFanu
Lumsdaine wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAAkwb-khw8jR-zUzG+kKeLt4uZZDW3=8A-vJenALRam8E=4Nrg@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div dir="ltr">On Wed, Dec 16, 2020 at 1:40 PM Thorsten
Altenkirch <<a
href="mailto:Thorsten.Altenkirch@nottingham.ac.uk"
moz-do-not-send="true">Thorsten.Altenkirch@nottingham.ac.uk</a>>
wrote:<br>
><br>
> But this is not the arrow category it is something else.<br>
<br>
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.
<div><br>
<div>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.
<div><br>
</div>
<div>I gave the main details of this in my talk at the
memorial conference for Erik Palmgren.<br>
Slides: <a
href="http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf"
moz-do-not-send="true">http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf</a><br>
Video: <a href="https://youtu.be/glC8tC7xdBY"
moz-do-not-send="true">https://youtu.be/glC8tC7xdBY</a>
<div><br>
</div>
<div>
<div style="color:rgb(0,0,0)">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).</div>
<div style="color:rgb(0,0,0)"><br>
</div>
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”.</div>
<div><br>
</div>
<div>–Peter.</div>
<div><br>
</div>
<div><br>
</div>
</div>
</div>
</div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>