<div dir="auto">This is very nice, thank you for sharing it, Daniel!<div dir="auto">/Sandro</div><div dir="auto"><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Feb 26, 2021, 02:59 Daniel Lee <<a href="mailto:laniel@seas.upenn.edu">laniel@seas.upenn.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi all,<div><br></div><div>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.<br><div><br></div><div>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 <a href="https://github.com/agda/cubical" target="_blank" rel="noreferrer">agda/cubical repo</a> 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). </div><div><br></div><div>Best,</div><div>Daniel</div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Dec 21, 2020 at 12:08 PM Anders Mortberg <<a href="mailto:andersmortberg@gmail.com" target="_blank" rel="noreferrer">andersmortberg@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The redundancy in the definition of category also pops up in most<br>
HoTT/UF libraries with some category theory:<br>
<br>
<a href="https://github.com/HoTT/HoTT/blob/master/theories/Categories/Category/Core.v#L40" rel="noreferrer noreferrer" target="_blank">https://github.com/HoTT/HoTT/blob/master/theories/Categories/Category/Core.v#L40</a><br>
<a href="https://unimath.github.io/doc/UniMath/4dd5c17/UniMath.CategoryTheory.Categories.html#is_precategory" rel="noreferrer noreferrer" target="_blank">https://unimath.github.io/doc/UniMath/4dd5c17/UniMath.CategoryTheory.Categories.html#is_precategory</a><br>
<a href="https://github.com/leanprover/lean2/blob/master/hott/algebra/category/precategory.hlean#L19" rel="noreferrer noreferrer" target="_blank">https://github.com/leanprover/lean2/blob/master/hott/algebra/category/precategory.hlean#L19</a><br>
<br>
I learned about this trick from the paper Jacques linked to and having<br>
C^op^op being strictly the same as C is indeed very useful. If someone<br>
prefers to avoid this trick then they should develop CT in Cubical<br>
Agda where it's not necessary as sym is strictly involutive. :-)<br>
<br>
--<br>
Anders<br>
<br>
On Mon, Dec 21, 2020 at 9:27 AM Nicolai Kraus <<a href="mailto:nicolai.kraus@gmail.com" target="_blank" rel="noreferrer">nicolai.kraus@gmail.com</a>> wrote:<br>
><br>
> Jacques and James, thanks for the explanations!<br>
><br>
> On 20/12/2020 22:16, James Wood wrote:<br>
> > The way stdlib is set up, you don't even get propositional equality<br>
> > without some extra work.<br>
><br>
> Thanks for pointing this out. I wasn't aware of it.<br>
> Asking the equivalence relation to be valued in h-props would be the<br>
> first step towards saturation in Peter's hierarchy. Adding groupoid<br>
> coherence laws would likely become insufficient after a while.<br>
><br>
> Nicolai<br>
><br>
> > To get a propositional equality from this to C .assoc f g h, we would<br>
> > need Setoid to give us some propositional equations. We could either<br>
> > enforce that the equivalence relation is h-prop-valued (probably the<br>
> > right thing) or add groupoid coherence laws. On top of that, we would<br>
> > need function extensionality.<br>
> ><br>
> > In any case, we should at least get an equivalence of categories,<br>
> > though I'm not sure how useful that is in practice in a non-univalent<br>
> > setting. In general, I think it's an interesting phenomenon that we<br>
> > can get ourselves into situations where judgemental equality is the<br>
> > only hope. The other example I can think of is how you can have a<br>
> > (badly behaved) category of Sets in plain Agda without using setoids<br>
> > because _∘_ is judgementally unital and associative.<br>
> ><br>
> > James<br>
> > _______________________________________________<br>
> > Agda mailing list<br>
> > <a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>