[Agda] Tips for working around proof relevance

[Nicolai Kraus]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201215/bb45738b/attachment.html>