I was reading this and I was trying to understand the definition of $(S,\Sigma)$-CCC. The first requirement says:

a mapping [[_]] : S → |C|, associating some object [[s]] ∈ |C| to any s ∈ S;

which I find very confusing and having a hard time understanding what it means. What is $S$ and what is $\Sigma$?

why do all the other requirements mean intuitively?


The meaning of $S$ and $\Sigma$ is defined on slide 6. $S$ is a set of base types (for example, natural numbers $\mathbb N$, Booleans $\mathbb N$, etc.): these are just formal symbols. $\Sigma$ is a set of operators, which included constants and functions (for example, $0 : \mathbb N$, $\text{true} : \mathbb B$, $\text{not} : \mathbb B \to \mathbb B$, etc.): these are pairs of an element of $S$ and a formal symbol. In the definition on slide 7, they seem to be limiting the operators to just constants.

The mapping $⟦-⟧ : S \to \mathrm{Ob}(\mathcal C)$ gives us an interpretation of a base type in the category $\mathcal C$: given any type $A \in S$, we have an object $⟦A⟧ \in \mathcal C$ interpreting that type.

They overload notation and also define a function $⟦-⟧: \Sigma \to \mathcal C^\to$. We interpret each constant $(c : A) \in \Sigma$ as a morphism $⟦c⟧: 1 \to ⟦A⟧$, where $1$ is the terminal object (called $\star$ in the lecture slides). This aligns with the usual interpretation of terms $\Gamma \vdash t : A$ as morphisms $⟦t⟧ : ⟦\Gamma⟧ \to ⟦A⟧$.

Together, both of these mappings $⟦-⟧$ allow us to interpret a signature for a simply-typed $\lambda$-calculus inside a cartesian-closed category, which is the first step in showing the equivalence between simply-typed $\lambda$-calculi and cartesian-closed categories.

| cite | improve this answer | |
  • $\begingroup$ Your answer ends abruptly. $\endgroup$ – Yuval Filmus Apr 16 at 15:26
  • $\begingroup$ @YuvalFilmus: thank you, I've fixed the answer. (I'm not quite sure how I managed to do that!) $\endgroup$ – varkor Apr 16 at 19:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.