Question

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.

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top