[WIP] Preadditive Categories

[TOTBWF]

Description

This PR implements Preadditive categories, in the style of Borceux¹. We also prove some properties, the most interesting of which surrounds biproducts. Traditional definitions of biproducts often require some sort of enrichment, or at the very least zero objects. However, recent developments by Karvonen² have provided an excellent definition that works without any sort extra structure, and coincides perfectly with older definitions when the enrichment is present.

Notes

Instead of defining Preadditive Categories as Ab-Enriched, we do the enrichment "by hand". This is done mainly to keep Preadditve (and in the future, Additive and Abelian) as structures over a category, rather than over an enriched one. This will allow us to show that the Category instances for Abelian Groups and modules over a Ring are Preadditive, rather than having to build a parallel instance that is Ab-Enriched.

Todos

• Show that the Ab-Enriched version is equivalent
• Show that our definition of biproducts implies the more traditional one

¹: Borceux, Handbook of Categorical Algebra, Volume 2, Definition 1.2.1
²: Karvonen, Biproducts without pointedness
https://arxiv.org/abs/1801.06488

[TOTBWF]

Ugh, moved to a new computer and git config is messed up. Will fix

[sstucki]

Nice work! I noticed the other day that we have CMon-enriched categories in the library:

agda-categories/src/Categories/Category/CMonoidEnriched.agda

Line 17 in c96e085

record CM-Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where

They are formalised in a similar way (by hand rather than via enrichment). Clearly they are related, so maybe the definition of preadditive categories should include the one for CMon-enriched ones? Or at least we should define a forgetful functor from one to the other. Similarly for the proof that these are equivalent to enriched categories, maybe the corresponding notions of tensor products could share some definitions/code.

WDYT?

[TOTBWF]

So I noticed the Communitive Monoid Enriched stuff when I was writing this, but there is one reason that I didn't include the definition in Preadditive. I've defined Preadditive as a property on an existing category, whereas CM-Category bundles up all of the fields from Category inside itself.

Now, this is part of a much larger design discussion, but my feelings these days is that most things like Preadditive should be defined as properties, rather than bundled structures. This is because of purely operational reasons: A lot of our existing definitions work over Category, so having things be properties when we can makes things more compositional and encourages re-use of definitions/theorems. Obviously some things should be bundled up (IE: Bicategory and friends), but I think these are largely exceptions from the norm.

With that in mind, perhaps a type that captures this sort of "enrichment by hand over some algebraic structure" could be useful. I'm not 100% what it would look like, but it's food for thought.

[sstucki]

So I noticed the Communitive Monoid Enriched stuff when I was writing this, but there is one reason that I didn't include the definition in Preadditive. I've defined Preadditive as a property on an existing category, whereas CM-Category bundles up all of the fields from Category inside itself.

I think the current convention — which is also the one used by the stdlib — is to have both an unbundled/property version (Is...) and a bundled one that uses the unbundled one internally. Things are slowly being migrated to this style. So maybe it would make sense to do this with both CM-Categories (add the unbundled version, e.g. CM-Enriched) and Preadditive (add a bundled version, e.g. PreadditiveCategory). I'll let @JacquesCarette and @HuStmpHrrr weigh in on this.

[JacquesCarette]

Very cool stuff. I will do a careful review soon. [The code is very clean, but we might as well optimize it even more while it's still under development.] Right now, I'll just comment on the various things that have already been discussed.

First: my attempt at CMon-enriched was partial. I'm trying to do tangent categories and the like, and was working incrementally and more or less directly from the sources. I'm not sure if 'my' way of doing it is good for scalability. We definitely should try to get these two to line up (i.e. use the same conventions), and I'm entirely willing to change mine if I made some sub-optimal choices. So yeah, if we can come up with a decent way to encode "enriched by hand over some algebraic structure", that would be grand.

Second: yes, we're moving to provide both bundled and unbundled versions. They have pros and cons, and it feels like a false choice to have to choose. It's just not that much work to provide both, and ends up way more useful in the end.

Third: I continue to prefer lots of small PRs over large ones. Even if the PRs have dependencies. So the (great!) infrastructure work in this PR should have been (can still be?) split. That work can be merged in much more quickly. The stuff that needs more careful consideration can then wait a bit longer, without stopping all progress.

[TOTBWF]

Sorry for dropping these big PRs, It is a bad habit! I'll spin of the biproduct + reasoning combinators into separate PRs.

[JacquesCarette]

No worries, I easily drift into that too. I then have to go back and do some git magic to fix my own bad habits.

[TOTBWF]

I've spun out Biproducts and the reasoning combinators into #250 and #251, respectively.

[themar7777]

Global

[JacquesCarette]

@TOTBWF I know this is rather an old, partial PR, and that you're working more on 1lab right now, but it would be nice to get some closure on this one (and I mean that in let's get it pulled in, not let's just close it!). Anything I can do to prod that along?

[TOTBWF]

To be honest I had totally forgotten about this! I'll try and get this over the finish line next week!

[JacquesCarette]

I guess "next week" didn't really happen... is there a chance this will get completed?