The previous attempt was based on the very general view currently sketched on nLab. Unfortunately, that view isn't worked out very much in the literature, so doing even fairly basic stuff would be new, substantial work.
So instead, do them 'as usual'. This forced the implementation of quite a few things (that were worthwhile):
"unbundled" categories (Categories.Category.Unbundled) which are Categories with Obj as a parameter instead of a field. This permits making two categories with evidently definitionally equal objects.
some utilities and properties (such as conversions, i.e. pack/unpack, with usual categories).
IdentityOnObjects 'functors', that are easy to define on "unbundled" categories
An instance of the category 'Nat' with objects natural numbers and morphism all Fin m -> Fin n functions. Coproducts and Cocartesian. And then, by Duality that Nat^op has products and is Cartesian.
Use all of the above to define Lawvere Theories, and the Category of Lawvere Theories.
Implement a couple of simple instances, called 'Triv' and 'Identity'. Interestingly, 'Triv' requires a lot more code (even though it's all trivial) than Identity.
The previous attempt was based on the very general view currently sketched on nLab. Unfortunately, that view isn't worked out very much in the literature, so doing even fairly basic stuff would be new, substantial work.
So instead, do them 'as usual'. This forced the implementation of quite a few things (that were worthwhile):
Categories.Category.Unbundled) which are Categories withObjas a parameter instead of a field. This permits making two categories with evidently definitionally equal objects.