4
$\begingroup$

I see how objects in a category stand for types, but where do I find the terms and more specifically the rules which tell me which of them are allowed? When I e.g. consider a Cartesian closed category as model of a type theory, how are term constructors represented?

I guess this is the same as asking how do I know or specify appropriately what the homsets of this category are, which I assume are in bijection with the lambda terms. The Curry–Howard–Lambek correspondence as presented at the end of the Wikipedia page Curry–Howard–Lambek correspondence presents all terms conventionally as in a type theory, but if I start out with a category, the model, then I must have specified them in a more algebraic sense.

And once given, does the model also represent $\beta$ and $\eta$ conversion? I actually read on the (quite too high level for me) nLab that morphisms relate to substitutions. Then I guess the lambda terms are somehow elements of the objects.

$\endgroup$

1 Answer 1

8
$\begingroup$

Your intuition is correct: terms are "somehow" elements of the objects. The only thing left is to figure out what elements in a category are. They cannot be literally elements because objects need not be sets (and more generally there may be no way to even "convert" an object to a set with a functor).

If I say "consider a mass point $p$ moving in $\mathbb{R}^3$" then you will immediately understand that $p$ is not actually an element of $\mathbb{R}^3$ but a map $\mathbb{R} \to \mathbb{R}^3$, i.e., the point is parameterized by time (which we take to be a real number). It is a general phenomenon that "entities" can be parameterized, and so they can be thought of as either variable elements or maps. For instance "temperature" may be thought of as a scalar field mapping the points of Earth's surface to real numbers, or it can be thought of as a real number which varies with position on the Earth.

In any case, this leads to the idea that the elements of an object $A$ in a category are simply all morphisms $B \to A$. When $B$ is the terminal object, we get the global (non-parameterized) elements, but in general we allow elements to be parameterized by any object, and so we call them generalized elements. One way to understand the Yoneda lemma is that an object in a category consists of its generalized elements.

You asked how to pass from a category to its internal type theory. Let me answer the opposite question first. Given a type theory, we can think of terms in context as the generalized elements of a type, while the closed terms are the global elements. But since generalized elements are the same thing as morphisms this tells us how to build a category out of a type theory: the morphisms are just terms in a context, quotiented by whatever equations the theory proves.

To go in the opposite direction, suppose we have a category $\mathcal{C}$ and we want to make a type theory out of it. As you said, we take the types to be the objects of $\mathcal{C}$. According to our view that "generalized elements are morphisms", the morphisms $f : A \to B$ ought to correspond to terms of type $B$ in context $A$. But we cannot just write $x : A \vdash f : B$ because there is no $x$ on the right-hand side. It would make more sense for $f$ to have the type $A \to B$, which is precisely what we do. For each morphism $f : A \to B$ we introduce a constant of type $A \to B$, which we also write as $f$. Then the correspondence is recovered: given $x : A$ there is a term $f\, x : B$.

If our type theory does not have arrow types then we have to do things a bit differently. For each morphisms $f : A \to B$ in $\mathcal{C}$ we add a unary term constructor $f$ and the typing rule $$\frac{\Gamma \vdash e : A}{\Gamma \vdash f\,e : B}.$$ Note that $f\,e$ is just a syntactic form, namely application of the unary term constructor $f$ to the term $e$. It would make no sense to apply the morphims $f$ to the term $e$! A type theory consists not only of types and terms, but also of equations. Our category gives us some equations, too: if the morphism $h : A \to C$ is the composition of $f : A \to B$ and $g : B \to C$, then we get the equation $$x : A \vdash h \, x =_C g (f \, x).$$ There are some further equations. For instance, if $A$ and $B$ are objects and $C$ is their product, then we need to relate the type $C$ with the product type $A \times B$. That is, in the category there are projections $\pi_1 : C \to A$ and $\pi_2 : C \to B$ and a pairing operation $\langle{-}, {-}\rangle$, while in type theory there are projections $\mathtt{fst} : A \times B \to A$ and $\mathtt{snd} : A \times B \to B$ and pairing $({-},{-})$ (where $A \times B$ is the formal product type). We need equations which relate these, but let me skip the technicalities.

The $\beta$ and $\eta$ reduction rules are validated by a cartesian closed category. The rules about product and function types correspond to various parts of the adjunction between cartesian products and exponentials.

In conclusion, it may seem strange that we take all morphisms in a category and make them into unary constructors of the corresponding type theory. If the category is very big that gives us a very large type theory which is not syntactic in any sense of the word syntactic. Just free your mind and the rest will follow.

$\endgroup$
8
  • $\begingroup$ Thanks for your answer! You say "One way to understand the Yoneda lemma is that an object in a category consists of its generalized elements." How does this work for an object in $\mathrm{Set}$, say $X=\{4,5,9\}$. Does this object consist of it's generalized elements? Has it to do with extensionality, $3^2=9$ etc.? / And regarding terms which are equal by $\beta/\eta$ reduction: Say $x,y,z:A$. When we asked the category theory, can it see that $fx$, $(\lambda y.fy)x$ and $(\lambda z.((\lambda y.fy)z)x$ are three different (but equal by reduction according to the type theory theory) terms? $\endgroup$
    – Nikolaj-K
    Dec 18, 2013 at 9:14
  • $\begingroup$ $Set$ is special because it is well-pointed so a set is already determined by its global elements, so Yoneda is an overkill. In $Set$ Yoneda would say: if $X$ and $Y$ are sets such that, for all sets $Z$, the functions $Z \to X$ are in bijective correspondence with functions $Z \to Y$, then $X$ and $Y$ are in bijective correspondence. This of course holds because we just take the case $Z = 1$, the singleton set. $\endgroup$ Dec 18, 2013 at 9:43
  • $\begingroup$ Regarding your second question: yes, the category can "see" that these terms all denote the same morphism. $\endgroup$ Dec 18, 2013 at 9:43
  • $\begingroup$ Okay so "consists" doesn't directly translate to "contains the elements" in the $Set$ case. / But how does the category even tell you of the existence of both $(λy.fy)x$ and $(λz.((λy.fy)z)x$? Both are in $A\to B$ and extentionally the same there. If you start with the category, how do you know that these two are terms. The judgement "$(λy.fy):B$" and "$(λz.((λy.fy)z)x:B$" can be followed from another, but they are different sentences in type theory. I don't know what these two strings correspond to in a category, when clearly both must somehow be formed from only $A,B$ and $\to$. $\endgroup$
    – Nikolaj-K
    Dec 18, 2013 at 10:30
  • $\begingroup$ Now you are just asking how to interpret simply typed $\lambda$-calculus in a category. Each term gets mapped to a morphism. Variables get mapped to projections, application corresponds to the evaluation morphism, and $\lambda$-abstraction corresponds to transposition of a morphism. This is completely standard, so I am not going to write it out here. You can find numerous places online where this is spelled out. The point is that the terms $f$, $\lambda y. f y$ and $(\lambda z . ((\lambda y . f y) z)$ correspond to the same morphism in the category. Why is this surprising? $\endgroup$ Dec 18, 2013 at 14:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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