<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body dir="auto">
Why are there hard to work with? Set-enriched categories are unnecessary when using cubical Agda!
<div><br>
</div>
<div>All this setoid stuff should be removed!</div>
<div><br>
</div>
<div>Thorsten<br>
<br>
<div dir="ltr">Sent from my iPhone</div>
<div dir="ltr"><br>
<blockquote type="cite">On 15 Dec 2020, at 02:16, Carette, Jacques <carette@mcmaster.ca> wrote:<br>
<br>
</blockquote>
</div>
<blockquote type="cite">
<div dir="ltr">
<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-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
<!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Categories defined using propositional equality are very hard to work with. I’m not surprised things went sideways.<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">Here’s a full construction of the Comma Category in Agda
<a href="https://agda.github.io/agda-categories/Categories.Category.Construction.Comma.html">
https://agda.github.io/agda-categories/Categories.Category.Construction.Comma.html</a><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">In Setoid-Enriched categories, we get to define what equivalent arrows are. In particular, the proofs are not part of the definition, and that makes life much simpler.<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">Recommendation: if you’re going to insist on using propositional equality, do yourself a favour, and use –with-K. That will already help. Eventually, you’ll likely have to assume function extensionality
as well.<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">Jacques<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-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> Agda <agda-bounces@lists.chalmers.se>
<b>On Behalf Of </b>Daniel Lee<br>
<b>Sent:</b> December 14, 2020 8:40 PM<br>
<b>To:</b> agda@lists.chalmers.se<br>
<b>Subject:</b> [Agda] Tips for working around proof relevance<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal">Hi everyone,<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I'm an undergraduate in CS, trying to use this winter break to learn category theory via Categories in Context (and hopefully topology and HoTT). I thought it would be cool to formalize in Agda at the same time. <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Here's the link to the Agda development for reference: </span><a href="https://github.com/dan-iel-lee/categories-in-agda">https://github.com/dan-iel-lee/categories-in-agda</a> . Relevant files
are probably "Core" and "Examples/Comma".<o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I've run into a roadblock, specifically with proving that the comma category is a category, but which I imagine could be an issue in the future as well.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I've defined the arrows in the category as:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">Σ[ (h , k) </span><span style="font-family:"Cambria Math",serif">∈</span><span style="font-family:"Courier New""> d
</span><span style="font-family:"Cambria Math",serif">⟶</span><span style="font-family:"Courier New"">ᴰ d' × e
</span><span style="font-family:"Cambria Math",serif">⟶</span><span style="font-family:"Courier New"">ᴱ e' ] f'
</span><span style="font-family:"Cambria Math",serif">∘</span><span style="font-family:"Courier New""> (</span><span style="font-family:"Cambria Math",serif">ℱ</span><span style="font-family:"Courier New""> h) ≡ (</span><span style="font-family:"Cambria Math",serif">𝒢</span><span style="font-family:"Courier New"">
k) </span><span style="font-family:"Cambria Math",serif">∘</span><span style="font-family:"Courier New""> f</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Where h and k are the component arrows, and the body of the Sigma is the commutativity condition. Defining composition and identity are relatively straightforward, but proving the left/right
unit and associativity properties become difficult because it requires proving that the identities are identified. And because there are a lot of steps, compositions,... involved, the Goal is super hard to read and I don't know where to start in trying to
prove it. I managed to work around it by enforcing that all the hom-sets are sets (in the sense that their identification types are all identical). Is there a nice way to prove this without using proof irrelevance though?</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">All help is very very appreciated. Thanks :)))</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Best,</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Daniel</span><o:p></o:p></p>
</div>
</div>
</div>
</div>
<span>_______________________________________________</span><br>
<span>Agda mailing list</span><br>
<span>Agda@lists.chalmers.se</span><br>
<span>https://lists.chalmers.se/mailman/listinfo/agda</span><br>
</div>
</blockquote>
</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>