[WIP] Add biproduct infrastructure for additive categories #2300
+185
−0
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Extracting Biproducts.v from stable categories formalization (HoTT#2288). **Status: WIP - not ready for merge** Changes from original formalization: - Fixed imports (removed non-existent ZeroMorphismLemmas.v) - Made `ZeroObject` implicit throughout using `` `{Z : ZeroObject C} `` - Updated `zero_morphism` calls to use implicit Z parameter - Removed unused definitions (bi_inl, bi_inr, bi_outl, bi_outr, biproduct) - Removed unused lemma (biproduct_prod_unique) - Applied HoTT style conventions The file provides: - `BiproductData`: injection/projection morphisms - `IsBiproduct`: axioms (beta_l, beta_r, mixed_l, mixed_r) - `HasBiproductUniversal`: universal properties as product and coproduct - `Biproduct`: complete structure combining the above - Operations: biproduct_coprod_mor, biproduct_prod_mor with beta lemmas - Uniqueness lemma: biproduct_coprod_unique @jdchristensen This is work in progress, naturally - submitting early for initial feedback. I will be continuously re-reviewing for anything I missed. Thank you very much for your time
Following patterns from ZeroObject, make Biproduct a Class to enable automatic inference. Add coercion from BiproductData to object which allows writing just (biproduct_data B) instead of the verbose (biproduct_obj (biproduct_data B)) throughout. Changes: - Change Record Biproduct to Class Biproduct for typeclass inference - Add Coercion biproduct_obj : BiproductData >-> object - Simplify all morphism type expressions using the new coercion - Style: use 1: instead of braces in biproduct_coprod_unique proof This brings the file in line with the patterns established in PR HoTT#2293.
- Move parameter to next line in HasBiproductUniversal (80 char limit) - Add coercion from Biproduct to BiproductData for cleaner API usage
Collaborator
jdchristensen
left a comment
jdchristensen
left a comment
There was a problem hiding this comment.
This is looking good! Just a few minor things.
Collaborator
|
@Alizter @JasonGross Do either of you know why the doc-dep-graphs build is failing? It happened on two PRs today. The error is |
Collaborator
|
@CharlesCNorton BTW, you said that this is WIP, but it looks fairly polished. If your plan is to add more, I recommend that we first address the comments above, and then merge this and do additional work in a followup PR. |
Contributor
|
The internet suggests this is an issue with cabal-install metadata being outdated, and that adding If that doesn't work, we can try (not sure if all these steps are needed) |
- Remove unnecessary `: Type` annotations from Records and Class - Add missing biproduct_prod_unique lemma for dual completeness - Name hypotheses in lemma signatures rather than using intros - Leverage coercion to write `B` instead of `biproduct_data B`
Per reviewer feedback, add biproduct_coprod_universal and biproduct_prod_universal definitions to avoid repeating @center expressions. Beta lemmas still use set/destruct due to Coq type inference limitations with mixed sigma/product types.
CharlesCNorton
added a commit
to CharlesCNorton/Coq-HoTT
that referenced
this pull request
Aug 2, 2025
Extracting AdditiveCategories.v from stable categories formalization (HoTT#2288). **Provides:** - `AdditiveCategory`: Categories with zero objects, biproducts, and abelian group structure on hom-sets - Helper functions for accessing biproduct components - Universal property operations with uniqueness (both product and coproduct) - `AdditiveFunctor`: Preserves zero objects, biproducts, and morphism addition - Main theorem: `additive_functor_preserves_zero_morphisms` - Identity and composition of additive functors **Changes from original:** - Fixed imports (removed non-existent ZeroMorphismLemmas.v) - Changed to `Class` with implicit `ZeroObject` instance - Added complete abelian group structure on hom-sets: - `add_morphism` operation with commutativity, associativity - Zero morphism as identity, existence of inverses - Bilinearity of composition (distributivity) - Removed 8 unused wrapper lemmas (e.g., `add_beta_l`, `add_mixed_r`) - Added `add_prod_unique` for product/coproduct duality - Updated transport lemma names to match Core.v - Applied HoTT style conventions Depends on: HoTT#2293 (ZeroObjects), HoTT#2300 (Biproducts) @jdchristensen The main new addition (no pun intended) is the abelian group structure on hom-sets, which makes this a proper additive category (not just a category with zero objects and biproducts). Also I have probably overlooked a few things. Will be looking over again, but wanted to get the PR submitted.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Extracting Biproducts.v from stable categories formalization (#2288).
Status: WIP - not ready for merge
Changes from original formalization:
ZeroObjectimplicit throughout using`{Z : ZeroObject C}zero_morphismcalls to use implicit Z parameterThe file provides:
BiproductData: injection/projection morphismsIsBiproduct: axioms (beta_l, beta_r, mixed_l, mixed_r)HasBiproductUniversal: universal properties as product and coproductBiproduct: complete structure combining the above@jdchristensen This is work in progress, naturally - submitting early for initial feedback. I will be continuously re-reviewing for anything I missed. Thank you very much for your time