[Agda] Tips for working around proof relevance

[Jesper Cockx]

How is https://odr.chalmers.se/bitstream/20.500.12380/256404/1/256404.pdf
for a solution?

-- Jesper

On Tue, Dec 15, 2020 at 11:05 AM 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201215/7f2c51a7/attachment.html>