[Agda] Tips for working around proof relevance

[Sandro Stucki]

> Why are there hard to work with? Set-enriched categories are unnecessary when using cubical Agda!
>
> All this setoid stuff should be removed!

That was not very constructive Thorsten.
I bet you can do better than just claiming the existence of a solution
to Daniel's problem in cubical Agda and actually provide one...

/Sandro


On Tue, Dec 15, 2020 at 10:39 AM Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
> Why are there hard to work with? Set-enriched categories are unnecessary when using cubical Agda!
>
> All this setoid stuff should be removed!
>
> Thorsten
>
> Sent from my iPhone
>
> On 15 Dec 2020, at 02:16, Carette, Jacques <carette at mcmaster.ca> wrote:
>
> 
>
> Categories defined using propositional equality are very hard to work with. I’m not surprised things went sideways.
>
>
>
> Here’s a full construction of the Comma Category in Agda https://agda.github.io/agda-categories/Categories.Category.Construction.Comma.html
>
>
>
> 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.
>
>
>
> 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.
>
>
>
> Jacques
>
>
>
> From: Agda <agda-bounces at lists.chalmers.se> On Behalf Of Daniel Lee
> Sent: December 14, 2020 8:40 PM
> To: agda at lists.chalmers.se
> Subject: [Agda] Tips for working around proof relevance
>
>
>
> Hi everyone,
>
>
>
> 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.
>
>
>
> Here's the link to the Agda development for reference: https://github.com/dan-iel-lee/categories-in-agda . Relevant files are probably "Core" and "Examples/Comma".
>
>
>
>
>
> 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.
>
>
>
> I've defined the arrows in the category as:
>
> Σ[ (h , k) ∈ d ⟶ᴰ d' × e ⟶ᴱ e' ] f' ∘ (ℱ h) ≡ (𝒢 k) ∘ f
>
>
>
> 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?
>
>
>
> All help is very very appreciated. Thanks :)))
>
>
>
> Best,
>
> Daniel
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
> 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.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda