<div dir="ltr"><div dir="ltr">On Wed, Dec 16, 2020 at 7:44 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div lang="EN-GB" style="overflow-wrap: break-word;">
<div class="gmail-m_8943112760388695649WordSection1">
<p class="MsoNormal"><span>It is something else because you can still observe the codes underlying the setoid </span></p></div></div></blockquote><div><br></div><div>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.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div lang="EN-GB" style="overflow-wrap: break-word;"><div class="gmail-m_8943112760388695649WordSection1"><p class="MsoNormal"><span>and you can define functions that do not repsect the steoid equality.</span></p></div></div></blockquote><div><br></div><div>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.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div lang="EN-GB" style="overflow-wrap: break-word;"><div class="gmail-m_8943112760388695649WordSection1"><p class="MsoNormal"><span><u></u><u></u></span></p>
<p class="MsoNormal">Setoids are ok once we hide them by making the mandatory. Mixing setoids and sets is harmful.</p>
<p class="MsoNormal"><span><u></u></span></p></div></div></blockquote><div><br></div><div>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.</div><div><br></div><div>Nicolai <br></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div lang="EN-GB" style="overflow-wrap: break-word;"><div class="gmail-m_8943112760388695649WordSection1"><p class="MsoNormal"><span> <u></u></span></p>
<p class="MsoNormal"><span>Thorsten<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border-right:none;border-bottom:none;border-left:none;border-top:1pt solid rgb(181,196,223);padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12pt;color:black">From: </span></b><span style="font-size:12pt;color:black">Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Peter LeFanu Lumsdaine <<a href="mailto:p.l.lumsdaine@gmail.com" target="_blank">p.l.lumsdaine@gmail.com</a>><br>
<b>Date: </b>Wednesday, 16 December 2020 at 16:22<br>
<b>To: </b>Thorsten Altenkirch <<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>><br>
<b>Cc: </b>"<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>Re: [Agda] Tips for working around proof relevance<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal">On Wed, Dec 16, 2020 at 1:40 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">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.<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal">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.<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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" target="_blank">
http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf</a><br>
Video: <a href="https://youtu.be/glC8tC7xdBY" target="_blank">https://youtu.be/glC8tC7xdBY</a><u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="color:black">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).<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="color:black"><u></u> <u></u></span></p>
</div>
<p class="MsoNormal">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”.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">–Peter.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<pre>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.



</pre></div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div>