I’ve been really having a hard time trying to understand categorical semantics. In fact, I am confused to the point I am afraid I don't know how to ask this question!
I’ve been reading textbooks like Makkai and Reyes’ book, Jacobs’ Categorical logic and type theory (1992) or Categorical Logic by Andrew Pitts, but I simply cannot get the feeling of what are they trying to do. This entry and this one in the nlab do not seem to be very helpful for my understanding. In fact, it seems that the more I read the more confused I get.
Can those questions be answered crystal clearly?
How we define a categorical interpretation?
If it a functor, what is its domain? That is, in model theory, we interpret languages. What are we interpreting here, languages or theories .. or something else?
Let me take an example: I know, very informally, that intuitionistic propositional logic (IPL) correspond to bicartesian closed categories (BCC).
- But how to make this statement mathematically precise? How do we define such an interpretation?
If it is indeed a functor, what is its domain? The category of intuitionistic propositional logics or the category of intuitionistic propositional languages? Or even a particular intuitionistic propositional logic understood as a categry (possibly given by the category of proofs)?
I would really appreciate any answer that could shed some light not only into this example, but also into the big picture of it.
Background: I believe to have all the required background in category theory (UPs, natural transformations, equivalences, adjoints etc.) and type theory (polymorphism, dependent types etc.), having attended courses in both disciplines.