Uses of categories for knowledge representation

Notes from chatting w/ Jabari:

Category theory is all about finding shared structures across different areas of math, to be able to say useful things about them and identify connections and common results. It offers a clear and sobering way of describing these things. What are examples of extending this outside of math to general-purpose knowledge?

  • Spivak and others are working on this at MIT. Performant Coq libraries (arXiv; github) for validating related claims have been around for some time.

Examples: object types; relations; have an initial representation where further inferrences from it are already in the data, or are meaningful within the original set of things described.