<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body dir="auto">
I can expect contributors to this list to master time travel, can’t I? :-)
<div><br>
</div>
<div>Apologies to Daniel!<br>
<br>
<div dir="ltr">Sent from my iPhone</div>
<div dir="ltr"><br>
<blockquote type="cite">On 16 Dec 2020, at 09:10, Nicolai Kraus <nicolai.kraus@gmail.com> wrote:<br>
<br>
</blockquote>
</div>
<blockquote type="cite">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">On Wed, Dec 16, 2020 at 7:36 AM 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_7214995057774638581WordSection1">
<p class="MsoNormal" style="margin-left:36pt">I think I'll try out the setoid approach Jacques suggested, it does seem like it could make things easier. Are there any major downsides to this approach which would be useful to know. I've heard of talk of "setoid
hell" before where you build up a ton of extra proof obligations. Should I be worried about that in this case?<u></u><u></u></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Thanks for ignoring me.</span></p>
</div>
</div>
</blockquote>
<div><br>
</div>
<div>Daniel wrote the cited sentences three hours before you even entered the discussion, Thorsten. This makes your complaint about being ignored pretty unfair. You can't expect that people can predict what you'd write in the future - at least not the people
who are new to this list! [1]</div>
<div>I agree with the rest of your message :-)</div>
<div><br>
</div>
<div>[1] (I obviously knew what you were going to say.)</div>
<div><br>
</div>
<div>Nicolai<br>
</div>
<div><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_7214995057774638581WordSection1">
<p class="MsoNormal"><span>Been there tried this. Ok, so we define a category with homsetoids. But what about the objects. Ah they are just a type i.e. Set in Agda? But then how do you construct the arrow category? Now arrows become objects so how do we turn
a setoid into a type? Ok we better turn the objects into setoids to. But now the arrow are a setoid indexed over a setoid. It is not hard to figure out what this is but by now most of the definition of a caegroy is about setoids. And if everything is a setoid
maybe we should just lift all operations on types on setoids. That is exactly what I have done in ’99 (and there are some recent papers about setoid type theory). However, this is basically the idea in cubical agda but you don’t stop at setoids but go on to
groupoids and higher groupoids. That is a type has elements, equalities, equalities of equalities and so on. This is what you need to know about HoTT/cubical type theory in a nutshell. However, if you want to reason about ordinary categories then you can cut
out all the higher order stuff by adding the condition that homsets satisfy UIP and you are basically saying that they are a setoid without having to make this explicitly. In particular I fail to see what the advantage of Jaques proposal could be, since you
can take the quotient of a type and an equivalence relation in cubical agda and there is absolutely no reason to mess up the definition of a category.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <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>
<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" style="margin-left:36pt"><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 Daniel Lee <<a href="mailto:laniel@seas.upenn.edu" target="_blank">laniel@seas.upenn.edu</a>><br>
<b>Date: </b>Tuesday, 15 December 2020 at 06:50<br>
<b>To: </b>"nicolai.kraus" <<a href="mailto:nicolai.kraus@gmail.com" target="_blank">nicolai.kraus@gmail.com</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" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">Hi Nicolai, Jacques,<u></u><u></u></p>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">Thanks for the pointers! I have indeed already had to assume function extensionality. <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">So just to make sure I understand correctly, the reason that associativity is impossible to prove in the "wild categories" setting is that you not only need associativity in the original category, but also a sort
of "second level" notion of associativity in the composition of the commutative diagrams? And the reason it goes through when you assume that hom-sets are sets is that any two commutative diagrams, as long as their components are the same, are now assumed
to be identical. Is that right?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">Then, is it possible to add this higher-dimensional coherence rather than removing higher-dimensional structure completely?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">I think I'll try out the setoid approach Jacques suggested, it does seem like it could make things easier. Are there any major downsides to this approach which would be useful to know. I've heard of talk of "setoid
hell" before where you build up a ton of extra proof obligations. Should I be worried about that in this case?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">Lastly, how would you recommend defining hom/represented functors? Currently, I've used a universe category parametrized by some level 'c' whose objects are 'Set c'. Will I run into similar issues with "wildness"
if I don't enforce that the objects in the category are sets?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">Thanks again for the help.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">Best,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">Daniel<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36pt">On Mon, Dec 14, 2020 at 7:22 PM Nicolai Kraus <<a href="mailto:nicolai.kraus@gmail.com" target="_blank">nicolai.kraus@gmail.com</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-top:none;border-right:none;border-bottom:none;border-left:1pt solid rgb(204,204,204);padding:0cm 0cm 0cm 6pt;margin-left:4.8pt;margin-right:0cm">
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12pt;margin-left:36pt">
Hi Daniel,<br>
<br>
nice Agda project! But using the winter break to learn category theory, topology, HoTT, AND to formalise things in Agda sounds pretty ambitious to me ;-)<br>
<br>
The short answer to your question is "no". There's no nice way to do this without the assumption that hom-sets are sets (or another assumption). Actually, there is just no way at all, not even an ugly one. It's not just involved and tedious and hard to read,
it's not provable. The comma category construction does not work for the notion of categories that you use.<br>
<br>
To see why, look at your Agda code:<br>
When you define the objects of the comma category, you need to use objects + morphisms of the original categories.<br>
When you define the morphisms of the comma category, you need to use morphisms + composition of the original categories.<br>
When you define composition in the comma category, you need composition + associativity of the original categories.<br>
Do you see where this is going? You always need "one level more" of the original categories than you currently define in the comma category.<br>
Thus, when you want to prove associativity for the comma category, you should expect that you need more than only associativity of the original categories: you also need the first coherence condition for associativity, known as "MacLane's pentagon". MacLane's
pentagon doesn't show up explicitly for standard categories (where it is automatic), but it shows up when you study e.g. bicategories. Something similar happens for the identity laws.<br>
<br>
The notion of categories that you currently consider is badly behaved. We call them "wild categories" (or "naive" or "incoherent" or "approximate"). They are higher-dimensional categories, but with almost all coherence structure removed. To understand why this
is bad, think about categories where you don't require composition to be associative: you can probably imagine that all sorts of constructions from standard category theory will break.<br>
<br>
Your approach to require hom-sets to be sets is the standard approach. It ensures that the categories behave like standard 1-categories. It implies MacLane's pentagon coherence and all other coherences. Thus, it's a really strong assumption, but it's the right
assumption if you want to do 1-category theory in this style. This is also how it's done in the HoTT book. I think this is equivalent to Jacques' approach with setoids, but I haven't checked this in detail. ("Equivalent" in the sense that the two approaches
should make the same constructions possible, not equivalent in terms of how tedious things can become.)<br>
<br>
"--with-K" would, of course, imply that hom-sets are sets. But it also would mean that the type of objects (and everything else) is a set. This is quite restrictive. For example, your development wouldn't capture univalent categories. I don't know whether the
added convenience would make up for the loss of generality.<br>
<br>
The issue that you found here is a pretty deep one. This issue, together with things that are very much related, causes the problem and motivates the constructions in this paper:<br>
<a href="https://arxiv.org/abs/2009.01883" target="_blank">https://arxiv.org/abs/2009.01883</a><br>
See also Section 3.2, "Deficiency of Wild/Incoherent Structure", for a discussion. Especially Example 9, which uses a slice category (special case of the comma category, where one can already see the issues).<br>
<br>
Best,<br>
Nicolai<br>
<br>
<u></u><u></u></p>
<div>
<p class="MsoNormal" style="margin-left:36pt">On 15/12/2020 01:40, Daniel Lee wrote:<u></u><u></u></p>
</div>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<p class="MsoNormal" style="margin-left:36pt">Hi everyone, <u></u><u></u></p>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">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. <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><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" target="_blank">https://github.com/dan-iel-lee/categories-in-agda</a>
. Relevant files are probably "Core" and "Examples/Comma".<u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">I've defined the arrows in the category as:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><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><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><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><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><span style="font-family:Arial,sans-serif">All help is very very appreciated. Thanks :)))</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><span style="font-family:Arial,sans-serif">Best,</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><span style="font-family:Arial,sans-serif">Daniel</span><u></u><u></u></p>
</div>
</div>
<p class="MsoNormal" style="margin-left:36pt"><br>
<br>
<u></u><u></u></p>
<pre style="margin-left:36pt">_______________________________________________<u></u><u></u></pre>
<pre style="margin-left:36pt">Agda mailing list<u></u><u></u></pre>
<pre style="margin-left:36pt"><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u><u></u></pre>
<pre style="margin-left:36pt"><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><u></u><u></u></pre>
</blockquote>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
</blockquote>
</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>
</blockquote>
</div>
</div>
</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>