search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.26k stars 192 forks source link

biproducts #2016

Open Alizter opened 4 months ago

Alizter commented 4 months ago

In this PR we define what we mean by a category having biproducts. We prove standard lemmas, monoidal structure, funtoriality results and duality.

cc @ThomatoTomato you might want to take a look at this since it is directly part of the abelian category formalization in #1929.

jdchristensen commented 4 months ago

Some of the comments in #1929 that aren't marked as resolved are about the file Biproducts.v. Have they been addressed here? (I haven't had time to take a look at this PR yet, but will do so soon.)

Alizter commented 4 months ago

@jdchristensen I don't remember. I will take a closer look ASAP.

Alizter commented 4 months ago

I'll reproduce the outstanding comments here so we can address them in one place:

  1. Regarding line 143:

    I think this argument about how cat_coprod_prod computes when composed with the inclusions and projections has appeared more than once, so it should be factored out as a lemma. Then, with the change that only uses r once (using catie_homotopic), maybe there is no longer a need to assert the various pieces?

I'll write down and use these lemmas. They can probably appear in Coproducts.v.

I need to think a bit more about the rest of the comments.

  1. Regarding line 907:

    I have a feeling that what you are doing here might overlap with cat_biprod_corec_rec. If cat_biprod_corec_rec is generalized to be about comparing two maps from a coproduct to a product, then maybe it exactly covers what you need here? Or maybe a slight variation gives a common generalization of both goals?

  2. In Biproducts.v, symmetry and associativity of biproducts is proved using that these hold for products. Then there is some work in showing that these maps respect the coproduct structure. I feel like this should be more formal. In a category with biproducts, every product is canonically a biproduct (as is every coproduct). This is because the biproduct and the product both satisfy the universal property of the product. So the maps showing that products are associative and symmetric, defined using the product structure, should "automatically" respect the coproduct structure. I'm not sure how to make this more precise in a way that would make the proofs simpler, but I suspect that there should be a way.

Alizter commented 1 month ago

@jdchristensen I haven't been able to make progress with the comments that we had, perhaps I no longer understand what needs to be done. Would you be able to take another look at this and give a fresh review, that should allow us to make some progress on this.

I would like to get this merged eventually, so that we can make room for the other abelian cat stuff.

jdchristensen commented 1 month ago

@Alizter It will take me some time to remember the context here. I might have time tomorrow, but if not, it will likely be next week.