1
$\begingroup$

In the article at nlab about the relation between type theory and category theory, it is said that "beta reduction" in type theory corresponds to "counit for hom-tensor adjunction" in category theory and also "substitution" corresponds to "composition of classifying morphisms / pullback of display maps" correspondingly.

Are these considered denotational or operational semantics?

$\endgroup$

Your Answer

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

Browse other questions tagged or ask your own question.