[Agda] Tips for working around proof relevance

Wed Dec 16 03:08:07 CET 2020

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 listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201216/f4454a54/attachment.html>