I am trying to work on a project where I define a formally verified model of a restaurant business. You can think of it like a model of a manufacturing process, production workflow of some kind, or organizational operation.
I really like the idea of ologs, which are category-theoretic knowledge graphs, essentially, but I am still thinking a lot about how to interpret them conceptually.
Some good advice I got is that you should be able to express your idea mathematically first before trying to code it.
That said, I’m curious to know how people think ologs fit best into Coq.
There is a paper on formalizing ologs that I should read.
Page 11 is where they give a mathematical foundation for ologs:
A type N = (N , T ) consists of a noun phrase N (see Definition 2.1.1) and an author set T such that T ⊧ N. The author set may be denoted Auth(N) ∶= T.
(b) Given two types N1 and N2, an aspect from N1 to N2, denoted V ∶ N1 → N2, consists of a pair V = (V , A), where V is a verb phrase functionally connecting N1 to N2 in the sense of Definition 2.1.3, where A is an author set such that A ⊆ Auth(N1)∩Auth(N2), and where A ⊧ V . The author set may be denoted Auth(V ) ∶= A.
(c) Given two types N1 and N2, and two aspects V1, V2 ∶ N1 → N2, a fact from V1 to V2, denoted V1 ⇒ V2, is given by an author set F ⊆ Auth(V1) ∩ Auth(V2) and an endorsement F ⊧ [V1 ≃ V2], in the sense of Definition 2.1.4. We allow an abuse of notation and write F ∶ V1 ⇒ V2.2
I’m thinking to get started I should look up or think about how to define categories in Coq, presumably inductively.