[Agda] Tips for working around proof relevance

[Daniel Lee]

Hi all,

Thanks again for all the insightful comments! I really wasn't expecting to
see this much discussion extending from my simple question; it was very
cool to hear about the different perspectives on/methods for working with
categories in a type theory.

If anyone's interested in taking a look, I ended up working on a 1-category
theory library for/in cubical agda, which just got merged into the agda/cubical
repo <https://github.com/agda/cubical> a couple days ago. As promised by
Anders above, involutivity of ^op follows definitionally without needing
any additional fields. And some other nice things ended up
happening definitionally, such as one side of the Yoneda natural
isomorphism (as it should).

Best,
Daniel

On Mon, Dec 21, 2020 at 12:08 PM Anders Mortberg <andersmortberg at gmail.com>
wrote:

> The redundancy in the definition of category also pops up in most
> HoTT/UF libraries with some category theory:
>
>
> https://github.com/HoTT/HoTT/blob/master/theories/Categories/Category/Core.v#L40
>
> https://unimath.github.io/doc/UniMath/4dd5c17/UniMath.CategoryTheory.Categories.html#is_precategory
>
> https://github.com/leanprover/lean2/blob/master/hott/algebra/category/precategory.hlean#L19
>
> I learned about this trick from the paper Jacques linked to and having
> C^op^op being strictly the same as C is indeed very useful. If someone
> prefers to avoid this trick then they should develop CT in Cubical
> Agda where it's not necessary as sym is strictly involutive. :-)
>
> --
> Anders
>
> On Mon, Dec 21, 2020 at 9:27 AM Nicolai Kraus <nicolai.kraus at gmail.com>
> wrote:
> >
> > Jacques and James, thanks for the explanations!
> >
> > On 20/12/2020 22:16, James Wood wrote:
> > > The way stdlib is set up, you don't even get propositional equality
> > > without some extra work.
> >
> > Thanks for pointing this out. I wasn't aware of it.
> > Asking the equivalence relation to be valued in h-props would be the
> > first step towards saturation in Peter's hierarchy. Adding groupoid
> > coherence laws would likely become insufficient after a while.
> >
> > Nicolai
> >
> > > To get a propositional equality from this to C .assoc f g h, we would
> > > need Setoid to give us some propositional equations. We could either
> > > enforce that the equivalence relation is h-prop-valued (probably the
> > > right thing) or add groupoid coherence laws. On top of that, we would
> > > need function extensionality.
> > >
> > > In any case, we should at least get an equivalence of categories,
> > > though I'm not sure how useful that is in practice in a non-univalent
> > > setting. In general, I think it's an interesting phenomenon that we
> > > can get ourselves into situations where judgemental equality is the
> > > only hope. The other example I can think of is how you can have a
> > > (badly behaved) category of Sets in plain Agda without using setoids
> > > because _∘_ is judgementally unital and associative.
> > >
> > > James
> > > _______________________________________________
> > > 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
> _______________________________________________
> 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/20210225/1910bf08/attachment.html>