[Agda] Tips for working around proof relevance

[Sandro Stucki]

This is very nice, thank you for sharing it, Daniel!
/Sandro


On Fri, Feb 26, 2021, 02:59 Daniel Lee <laniel at seas.upenn.edu> wrote:

> 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
>>
> _______________________________________________
> 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/20210227/fea41098/attachment.html>