You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Julius Hamilton (Nov 28 2024 at 20:17):This is a very, very good book: https://global.oup.com/academic/product/modal-homotopy-type-theory-9780198853404?cc=us&lang=en& I expect it to inform the following question, but I also want to open it for discussion here.
I don't actually know to what extent Spivak was the originator of the idea that categories can be used as ontologies, since the connections between category theory, logic, and type theory was being studied actively in I think the 70's; and obviously, the interplay between logic and ontologies is discernible as far back as Aristotle.
When one tries to model an everyday conceptual system, there are much more fundamental concepts they make use of, to define the more familiar things in. So for example, for the migratory patterns of birds, the functioning of an economy, or whatever, one is inevitably dissecting the phenomenon into metaphysical categories such as "entities", "states", "attributes", "types", "processes", etc. The range of possibilities and questions for how to think about reality itself has lately been called "meta-metaphysics", but in the setting of formal ontologies, is called "upper ontologies".
As of late, I am struggling to choose a default or preferred upper ontology, to do some formal modeling in. Here is a passage which gives me hope that other people are working on this:
I would like to know if people have anything to say about if homotopy type theory / modal homotopy type theory is particularly well-suited for certain upper ontologies, and why.
David Corfield (Nov 29 2024 at 12:14):Thanks for the praise!
I think there are some interesting things to think about with regard to ontology. As you'll have seen, amongst the dependent type theory for natural language community, there's a division between those who want types for each common noun and those who want to carve out subtypes from a master type 'Entity':
image.png
But even that latter group seem to want to allow a range of basic types:
image.png
Of course, there's plenty of work not using dependent type theory which looks to determine the fundamental ontological categories, for instance, the DOLCE program. There's perhaps some useful work to be done starting from their taxonomy, but using dependent types rather than first-order logic:
image.png
