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.