Question: 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](https://ncatlab.org/nlab/show/categorical+semantics) entry and [this](https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory) 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.

Answer: 
There are (at least) two different sort of things you can do, roughly corresponding to syntax and semantics.

---

You can study the *internal logic* of a category, which lets you use a logical language as a convenient tool for doing calculations with in a category. e.g. objects are types, propositions are subobjects, et cetera.

Conversely, given a suitable language, we can construct its *syntactic category* consisting of all the types you can construct in the language and the functions you can define between them, and satisfying all of the relations you can prove hold between them. And thus we can use category theory to help us think of type theories.

---

On the semantic side we can think of a category $T$ (possibly with extra structure; e.g. a *sketch*) as being a theory. Then models of this theory in a category $C$ will be functors $F : T \to C$ of a certain type.

---

Of course, these aren't unrelated; if we have the theory of a group, we might then construct $T$ to be its syntactic category, and require the functors defining models of $T$ to be of the sort that preserves the logic used.

Conversely, if we're in the habit of studying functors out of some category $T$, it may be worth considering the theory given by internal language of $T$ and view functors as being models of that theory.

A common type of this construction is one we can do with universal algebra (e.g. the theory of groups, given as operations and equations). If we have some variety of universal algebra, we can take $T$ to be the opposite category of the category of finitely presented algebras, and then models will be functors from $T$ that preserve finite limits.
To address your comment that

> 
> that intuitionistic propositional logic (IPL) correspond to
>  bicartesian closed categories (BCC)
> 
> 
> 

the basic idea (and which is similar in other examples of categorical semantics of this sort) is to give a category of sufficiently structured categories $\mathfrak{C}$ (corresponding to the models of our logic) with the morphisms being the morphisms which preserve the logical structure. In the case of IPL, it should be functors which preserve finite products and coproducts.

Let's say by IPL we understand IPL with some atomic propositions $A\_1, A\_2, \dots$. So each object in $\mathfrak{C}$ should be a bicartesian closed category with an object $A\_i^{\mathcal{C}}$ for each atomic proposition $A\_i$ and the functors should additionally preserve the interpretation of these symbols. That is, $F : \mathcal{C} \to \mathcal{D}$ is a morphism in $\mathfrak{C}$ if $F$ preserves products and coproducts and $F(A\_i^\mathcal{C}) = A\_i^\mathcal{D}$.

Our logic itself corresponds to the initial object $0$ in this category. The objects of $0$ will just be the strings generated by the grammar
$s = A\_i \;|\; s \times s \;|\; s + s \;|\; \top \;|\; \bot $.

The maps in $\mathrm{Hom}\_0(X, Y)$ should just be the terms of type $X \to Y$ (where the objects of $0$ are interpreted as types in the obvious way, giving no introduction or elimination rules for the $A\_i$) in the simply typed lambda calculus with tuples and sums, modulo I think extensional equality.