Closed olynch closed 1 week ago
@olynch, I realized that there is a conceptual problem with the new design that I didn't detect in my first review. The problem is that:
FgCategory
is being thought of as describing bare categories (categories without extra structure) since object generators are identified with objects. Thus, it would not make sense to write, say, FgMonoidalCategory: FgCategory
because in a finitely generated monoidal category, the objects and the object generators will not coincide.FgDblModel
should apply to models of double theories beyond discrete ones (or else what is the point of having a trait on top of the struct DiscreteDblModel
), yet it extends FgCategory
. But this means that it identifies objects and object generators, which won't be the case for double theories with nontrivial object operations.I see two possible solutions:
FgCategory
by adding an ObGen
associated type, orFgDblModel
directly add the types it needs rather than extending FgCategory
.I'm inclined toward (1).
OK, for now I'm going to revert to using "Hom" to describe the external identities in a double theory. I'm open to revising this terminology in a future PR but it needs to be done carefully and consistently throughout the codebase and documentation, and the present state of this PR is quite far from that.
This compiles, but doesn't pass lints. The idea behind this refactor is that we should be more explicit in our traits about finitely-generated categories and double theory models. Specifically, "finitely generated" traits should expose actual implementations of FinGraph. This is in accordance with what "finitely generated" means mathematically for categories.
Default TODO list
dev-docs/
?