[Agda] Tips for working around proof relevance

[Daniel Lee]

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/20201214/31068b4e/attachment.html>