Comparison of conceptual / spiritual core
- CatColab: double Lawvere theories
- Catlab.jl: GAT
- Overlap of two mathematical backgrounds
- there’s considerable overlap in the purposes and capabilities
- but double theories are substantially different
- the system is not syntactic in the type-theoretic sense, although you could get at it with type theories
- every double theory has a whole double category of models, rather than a mere category
There’s considerable overlap in the purposes and capabilities of the two mathematical backgrounds, but double theories are substantially different; in particular the system is not syntactic in the type-theoretic sense, although you could get at it with type theories, but on the other hand every double theory has a whole double category of models, rather than a mere category, which is really helpful for many of the things we want to model.
- related, mentioned: double theories, double category