<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">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">http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf</a><br>Video: <a href="https://youtu.be/glC8tC7xdBY">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>