[Agda] Tips for working around proof relevance

[Anders Mortberg]

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