<div dir="ltr">Hi everyone,<div><br></div><div>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. </div><div><br></div><div><div><font face="arial, sans-serif">Here's the link to the Agda development for reference: </font><a href="https://github.com/dan-iel-lee/categories-in-agda">https://github.com/dan-iel-lee/categories-in-agda</a> . Relevant files are probably "Core" and "Examples/Comma".</div></div><div><br></div><div><br></div><div>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.</div><div><br></div><div>I've defined the arrows in the category as:</div><div><font face="monospace">Σ[ (h , k) ∈ d ⟶ᴰ d' × e ⟶ᴱ e' ] f' ∘ (ℱ h) ≡ (𝒢 k) ∘ f</font></div><div><font face="monospace"><br></font></div><div><font face="arial, sans-serif">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?</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">All help is very very appreciated. Thanks :)))</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">Best,</font></div><div><font face="arial, sans-serif">Daniel</font></div></div>