[Agda] Tips for working around proof relevance

[Thorsten Altenkirch]

I am just unhappy with Jacques proposing an outdated approach. The definition of a category is completely standard the only additional equation you need is to make sure that homsets are actually sets, i.e. you have to add one extra constructor. These are precategories in the sense of the HoTT book. You may want to add an additional axiom to state that the category is univalent (basically saying that isomorphism and equality agree) - that is what is called a category in HoTT. I prefer the terminology category / univalent category.

Nicolai gave a more constructive answer, so indeed you need to add the condition that homsets are sets. Otherwise you are not working with categories.
Another alternative would be to add K but this is currently inconsistent with cubical. There should be a version of cubical without glue, i.e. without univalence but still with propositional extensionality which is consistent with K. You can fake it but officially you would be inconsistent. 

I am just bothered that people still advertising setoids where we have something much better now. Next I suggest to program in Cobol...

Thorsten

On 15/12/2020, 10:05, "Sandro Stucki" <sandro.stucki at gmail.com> wrote:

    > Why are there hard to work with? Set-enriched categories are unnecessary when using cubical Agda!
    >
    > All this setoid stuff should be removed!

    That was not very constructive Thorsten.
    I bet you can do better than just claiming the existence of a solution
    to Daniel's problem in cubical Agda and actually provide one...

    /Sandro


    On Tue, Dec 15, 2020 at 10:39 AM Thorsten Altenkirch
    <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
    >
    > 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.
    >
    >
    >
    > _______________________________________________
    > 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.