<div dir="ltr"><div>How is <a href="https://odr.chalmers.se/bitstream/20.500.12380/256404/1/256404.pdf">https://odr.chalmers.se/bitstream/20.500.12380/256404/1/256404.pdf</a> for a solution?</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Dec 15, 2020 at 11:05 AM Sandro Stucki <<a href="mailto:sandro.stucki@gmail.com">sandro.stucki@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">> Why are there hard to work with? Set-enriched categories are unnecessary when using cubical Agda!<br>
><br>
> All this setoid stuff should be removed!<br>
<br>
That was not very constructive Thorsten.<br>
I bet you can do better than just claiming the existence of a solution<br>
to Daniel's problem in cubical Agda and actually provide one...<br>
<br>
/Sandro<br>
<br>
<br>
On Tue, Dec 15, 2020 at 10:39 AM Thorsten Altenkirch<br>
<<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br>
><br>
> Why are there hard to work with? Set-enriched categories are unnecessary when using cubical Agda!<br>
><br>
> All this setoid stuff should be removed!<br>
><br>
> Thorsten<br>
><br>
> Sent from my iPhone<br>
><br>
> On 15 Dec 2020, at 02:16, Carette, Jacques <<a href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>> wrote:<br>
><br>
> <br>
><br>
> Categories defined using propositional equality are very hard to work with. I’m not surprised things went sideways.<br>
><br>
><br>
><br>
> Here’s a full construction of the Comma Category in Agda <a href="https://agda.github.io/agda-categories/Categories.Category.Construction.Comma.html" rel="noreferrer" target="_blank">https://agda.github.io/agda-categories/Categories.Category.Construction.Comma.html</a><br>
><br>
><br>
><br>
> 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.<br>
><br>
><br>
><br>
> 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.<br>
><br>
><br>
><br>
> Jacques<br>
><br>
><br>
><br>
> From: Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> On Behalf Of Daniel Lee<br>
> Sent: December 14, 2020 8:40 PM<br>
> To: <a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a><br>
> Subject: [Agda] Tips for working around proof relevance<br>
><br>
><br>
><br>
> Hi everyone,<br>
><br>
><br>
><br>
> 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.<br>
><br>
><br>
><br>
> Here's the link to the Agda development for reference: <a href="https://github.com/dan-iel-lee/categories-in-agda" rel="noreferrer" target="_blank">https://github.com/dan-iel-lee/categories-in-agda</a> . Relevant files are probably "Core" and "Examples/Comma".<br>
><br>
><br>
><br>
><br>
><br>
> 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.<br>
><br>
><br>
><br>
> I've defined the arrows in the category as:<br>
><br>
> Σ[ (h , k) ∈ d ⟶ᴰ d' × e ⟶ᴱ e' ] f' ∘ (ℱ h) ≡ (𝒢 k) ∘ f<br>
><br>
><br>
><br>
> 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?<br>
><br>
><br>
><br>
> All help is very very appreciated. Thanks :)))<br>
><br>
><br>
><br>
> Best,<br>
><br>
> Daniel<br>
><br>
> _______________________________________________<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>
><br>
> This message and any attachment are intended solely for the addressee<br>
> and may contain confidential information. If you have received this<br>
> message in error, please contact the sender and delete the email and<br>
> attachment.<br>
><br>
> Any views or opinions expressed by the author of this email do not<br>
> necessarily reflect the views of the University of Nottingham. Email<br>
> communications with the University of Nottingham may be monitored<br>
> where permitted by law.<br>
><br>
><br>
><br>
> _______________________________________________<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>
_______________________________________________<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>