Parameterised categories

[varkor]

It would be useful to be able to describe categories that are parameterised by other categories. E.g. functor categories, which are parameterised by two categories, or the Ind-completion, which is parameterised by one category. I appreciate this would increase the complexity of the deduction logic, but it would be very useful in practice (and would be a good way to generate combinations of properties/non-properties).

[ScriptRaccoon]

This is a very interesting thought. We then probably also want to add implications like "If $C$ is small and $D$ is locally small, then $[C,D]$ is locally small".

When taking this and your other ideas to the end, they seem to be an attempt to incorporate all of (basic) category theory into CatDat. Probably every result of (basic) category theory can be broken down to something of the form "If object A of type T satisfies P1,...,Pn of type S, then it satisfies Q". So we may add objects of type T and S to CatDat (with corresponding tables), and also the implication P1 + ... + Pn => Q between objects of type S.

It would be cool to have this, but tbh I don't know how to do this without blowing up the project (and, even more so, the UI).