<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="blue" vlink="purple" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">It is something else because you can still observe the codes underlying the setoid and you can define functions that do not repsect the steoid equality.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Setoids are ok once we hide them by making the mandatory. Mixing setoids and sets is harmful.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thorsten<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;color:black">Agda <agda-bounces@lists.chalmers.se> on behalf of Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com><br>
<b>Date: </b>Wednesday, 16 December 2020 at 16:22<br>
<b>To: </b>Thorsten Altenkirch <psztxa@exmail.nottingham.ac.uk><br>
<b>Cc: </b>"agda@lists.chalmers.se" <agda@lists.chalmers.se><br>
<b>Subject: </b>Re: [Agda] Tips for working around proof relevance<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></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">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.<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></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">
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><o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></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).<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></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”.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">–Peter.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></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></body>
</html>