Is the Packaging Mathematical Structures paper still a good starting point for implementing a hierarchy of theories in a composable way? Are there modern features in the intervening 11 years that can make it nicer?

I think that this paper is now nicely complemented by https://arxiv.org/abs/2002.00620.

and the future might be https://github.com/math-comp/hierarchy-builder but it depends on what your purpose is

Awesome! These look great

(there is also https://math-comp.github.io/competing-inheritance-paths-in-dependent-type-theory/ but that might be more specialized)

@Shea Levy I recently gave hierarchy-builder a try and it can already do more than I would want to do manually. There may be some minor issues here and there (like documentation being scarce and not always up to date), but it's definitely worth trying.

There is a zulip channel for hierarchy builder, if you have any troubles.

Also, the master branch is in heavy development, so not very stable, but supports structures with parameters.

@Shea Levy the other approach is https://arxiv.org/abs/1102.1323

And tradeoffs are complex.

But if you want to live in the math-comp ecosystem, CSes are probably what you want.

@Paolo Giarrusso Ah, I don't really have any dependency on math-comp, just trying to learn best practices. Just described my use case a bit more here

Paolo Giarrusso said:

But if you want to live in the math-comp ecosystem, CSes are probably what you want.

What does "CS" refer to here by the way?

canonical structures

Last updated: May 24 2024 at 23:01 UTC