Skip to content

Identify properties by ID and type#263

Merged
ScriptRaccoon merged 2 commits into
mainfrom
property-table-design
Jul 4, 2026
Merged

Identify properties by ID and type#263
ScriptRaccoon merged 2 commits into
mainfrom
property-table-design

Conversation

@ScriptRaccoon

@ScriptRaccoon ScriptRaccoon commented Jul 3, 2026

Copy link
Copy Markdown
Owner

An issue that already became apparent while working on #242 was that, sooner or later, properties can no longer be identified solely by their ID in the database, i.e. by their name, since the same name can be used for properties of different structure types. For example:

regular category != regular functor

Thus, we cannot have a single entry with the primary key regular in the properties table (which, after #242, contains properties of all structure types). Other examples that will become problematic once additional structure types are added include:

initial functor != initial object
isomorphism (as a property of a morphism) != isomorphism (as a property of a functor)
cocomplete category != cocomplete monoidal category

To fix this, the primary key of the properties table is now the composite key (id, type). As a result, a couple of queries (though not many) had to be adjusted. (Of course, using a longer single primary key like regular_category is inconvenient.)

Remark: the structures table and the property_assignments table remain unchanged, even though one could argue that, for consistency, the type should also become part of their primary keys. This is not necessary at the moment, and if the need arises, it can be addressed in a later PR.

To demonstrate that the change works, the new functor properties "regular" and "coregular" have been added. Both properties have been decided for all functors in the database. (In fact, this motivated adding the property of preserving regular epis/monos in #262, which was merged recently.)

Other examples that may be added later: "additive functor" (can now be distinguished from "additive category"), "accessible functor" (can now be distinguished from "accessible category"), "cartesian functor", "topological functor", etc.

this proves that now different properties can have the same name across different structure types (regular functor != regular category), implemented in the previous commit
@ScriptRaccoon ScriptRaccoon force-pushed the property-table-design branch from 1a57872 to 00af974 Compare July 3, 2026 18:32
@ScriptRaccoon ScriptRaccoon merged commit 2bf31fa into main Jul 4, 2026
1 check passed
@ScriptRaccoon ScriptRaccoon deleted the property-table-design branch July 4, 2026 07:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant