[Agda] Tips for working around proof relevance

[Carette, Jacques]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201215/4ff1df56/attachment.html>