[Agda] Tips for working around proof relevance
carette at mcmaster.ca
Tue Dec 15 03:16:28 CET 2020
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.
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
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 :)))
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda