[Agda] Tips for working around proof relevance

[Anders Mortberg]

Hi Daniel,

I don't think you need to know too many details about Cubical Agda to
develop basic category theory. The agda/cubical currently has a very
tiny category theory library so any contributions are most welcome and
there's plenty of low-hanging fruit:

https://github.com/agda/cubical/tree/master/Cubical/Categories

Feel free to drop me an email and I can give you some concrete
suggestions for things to do and where to start in case you're
interested.


Btw, in my experience univalence is not really necessary when
developing the theory of non-univalent 1-categories. So working with
postulated funext and hom-sets is really like working in HoTT. What
Cubical Agda offers is a version of this system where funext is not a
postulate and one has some new primitives for working with
paths/equalities. The only caveat is that you cannot pattern-match on
paths/equalities using Agda's nice pattern-matching, but in my
experience this is a very small price to pay for all the cubical
features. You can of course still use J/path-induction manually, but
it turns out that you almost never want to do this as most things can
be proved more directly.

--
Anders

On Wed, Dec 16, 2020 at 4:39 AM Daniel Lee <laniel at seas.upenn.edu> wrote:
>
> Thank you, this is very helpful! I was thinking about trying cubical Agda, but was a little reluctant since I like to completely understand how things work before using it; i.e. after understanding HoTT and cubical type theory. I'll check it out, but I think I'll most likely try sticking to standard Agda postulating functional extensionality and with the added 'set' requirement for now.
>
> Thanks all for the input!
>
> Best,
> Daniel
>
> On Tue, Dec 15, 2020 at 6:08 PM Nicolai Kraus <nicolai.kraus at gmail.com> wrote:
>>
>> On Tue, Dec 15, 2020 at 6:49 AM Daniel Lee <laniel at seas.upenn.edu> wrote:
>>>
>>> So just to make sure I understand correctly, the reason that associativity is impossible to prove in the "wild categories" setting is that you not only need associativity in the original category, but also a sort of "second level" notion of associativity in the composition of the commutative diagrams?
>>
>>
>> Yes, that's right.
>>
>>>
>>> And the reason it goes through when you assume that hom-sets are sets is that any two commutative diagrams, as long as their components are the same, are now assumed to be identical. Is that right?
>>
>>
>> Exactly!
>>
>>>
>>> Then, is it possible to add this higher-dimensional coherence rather than removing higher-dimensional structure completely?
>>
>>
>> Yes, it's possible. But then you're not using ordinary categories (a.k.a. 1-categories a.k.a. categories) anymore, then you would work with generalizations. There are many different such generalizations of 1-categories, an overview is here:
>> https://ncatlab.org/nlab/show/higher+category+theory
>> These generalizations are more powerful and (in many situations) more useful than 1-categories, but also more complicated and often harder to work with. It's a trade-off, as always. The generalization that I'm most interested in is (infinity,1)-categories [see nLab link above] because this is the simplest well-behaved notion of category which the type-theoretic universe is an instance of. Put differently, if you want to work with a well-behaved notion of category and you need the universe to be such a category, then you either need to make an assumption such as --with-K, or you need to go to at least (infinity,1)-categories. If you don't want to go there and work with 1-categories, you can restrict the universe to h-sets; this will be a perfectly fine 1-category.
>> Adding the coherences is hard in practice and in theory, see here for approaches:
>> https://arxiv.org/abs/1707.03693  (popl'18)
>> https://arxiv.org/abs/2009.01883
>>
>>>
>>> I think I'll try out the setoid approach Jacques suggested, it does seem like it could make things easier. Are there any major downsides to this approach which would be useful to know. I've heard of talk of "setoid hell" before where you build up a ton of extra proof obligations. Should I be worried about that in this case?
>>
>>
>> I think the options that you have are:
>> (1) the approach you currently use, i.e. standard Agda, postulate function extensionality
>> (2) use setoids for the hom-sets of categories
>> (3) use cubical Agda with sets (h-sets) for the hom-sets.
>> Some people here have voiced some pretty strong opinions. I'm not the right person to give advice on how to implement things, but I personally would definitely check out possibility 3. 1&2 can certainly work, and people here have done it very successfully with these strategies, but 1&2 have drawbacks that you've already encountered or heard of. In comparison, cubical Agda allows you to do things in a clean and conceptually satisfying way.
>>
>>>
>>> Lastly, how would you recommend defining hom/represented functors? Currently, I've used a universe category parametrized by some level 'c' whose objects are 'Set c'. Will I run into similar issues with "wildness" if I don't enforce that the objects in the category are sets?
>>
>>
>> It really depends on the definition of category that you want to work with. My suggestion would be to use 1-categories (not the generalizations, save that for later), where you require the hom-sets to be sets, as you already did. If you do this, 'Set' (or 'Set c') is not a category, so what you've written doesn't even type check anymore. But 'Set' restricted to sets (i.e. Sigma(A : Set). is-set(A)) works just fine as a replacement.
>>
>> Cheers,
>> Nicolai
>>
>>
>>>
>>> Thanks again for the help.
>>>
>>> Best,
>>> Daniel
>>>
>>> On Mon, Dec 14, 2020 at 7:22 PM Nicolai Kraus <nicolai.kraus at gmail.com> wrote:
>>>>
>>>> Hi Daniel,
>>>>
>>>> nice Agda project! But using the winter break to learn category theory, topology, HoTT, AND to formalise things in Agda sounds pretty ambitious to me ;-)
>>>>
>>>> The short answer to your question is "no". There's no nice way to do this without the assumption that hom-sets are sets (or another assumption). Actually, there is just no way at all, not even an ugly one. It's not just involved and tedious and hard to read, it's not provable. The comma category construction does not work for the notion of categories that you use.
>>>>
>>>> To see why, look at your Agda code:
>>>> When you define the objects of the comma category, you need to use objects + morphisms of the original categories.
>>>> When you define the morphisms of the comma category, you  need to use morphisms + composition of the original categories.
>>>> When you define composition in the comma category, you need composition + associativity of the original categories.
>>>> Do you see where this is going? You always need "one level more" of the original categories than you currently define in the comma category.
>>>> Thus, when you want to prove associativity for the comma category, you should expect that you need more than only associativity of the original categories: you also need the first coherence condition for associativity, known as "MacLane's pentagon". MacLane's pentagon doesn't show up explicitly for standard categories (where it is automatic), but it shows up when you study e.g. bicategories. Something similar happens for the identity laws.
>>>>
>>>> The notion of categories that you currently consider is badly behaved. We call them "wild categories" (or "naive" or "incoherent" or "approximate"). They are higher-dimensional categories, but with almost all coherence structure removed. To understand why this is bad, think about categories where you don't require composition to be associative: you can probably imagine that all sorts of constructions from standard category theory will break.
>>>>
>>>> Your approach to require hom-sets to be sets is the standard approach. It ensures that the categories behave like standard 1-categories. It implies MacLane's pentagon coherence and all other coherences. Thus, it's a really strong assumption, but it's the right assumption if you want to do 1-category theory in this style. This is also how it's done in the HoTT book. I think this is equivalent to Jacques' approach with setoids, but I haven't checked this in detail. ("Equivalent" in the sense that the two approaches should make the same constructions possible, not equivalent in terms of how tedious things can become.)
>>>>
>>>> "--with-K" would, of course, imply that hom-sets are sets. But it also would mean that the type of objects (and everything else) is a set. This is quite restrictive. For example, your development wouldn't capture univalent categories. I don't know whether the added convenience would make up for the loss of generality.
>>>>
>>>> The issue that you found here is a pretty deep one. This issue, together with things that are very much related, causes the problem and motivates the constructions in this paper:
>>>> https://arxiv.org/abs/2009.01883
>>>> See also Section 3.2, "Deficiency of Wild/Incoherent Structure", for a discussion. Especially Example 9, which uses a slice category (special case of the comma category, where one can already see the issues).
>>>>
>>>> Best,
>>>> Nicolai
>>>>
>>>>
>>>> On 15/12/2020 01:40, Daniel Lee wrote:
>>>>
>>>> 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
>>>>
>>>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda