[Agda] Tips for working around proof relevance

[Thorsten Altenkirch]

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.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201215/a79eea3a/attachment.html>