In the article at nlab about relation between category theory and type theory, it is said that substitution in type theory is the same as composition of classifying morphisms in category theory.

Can you please explain why that is so for a newbie? And ellaborating on what exactly a classifying morphism is?!

  • 2
    $\begingroup$ It isn't. Substitution of a term into a term is just composition of morphisms, while substutution of a term into a type is pullback (or its analogue if we're working in a general fibration). $\endgroup$ Commented Nov 12, 2019 at 20:50
  • $\begingroup$ @Andrej So you mean what it says on nLab is wrong? Or there is something I misunderstood? $\endgroup$
    – al pal
    Commented Nov 12, 2019 at 21:46
  • $\begingroup$ I just wouldn't worry too much about that particular bit. It can probably be interpreted in a sensible way, but you shouldn't get hung up on little details, such as an entry in a table on a wiki. $\endgroup$ Commented Nov 12, 2019 at 22:13
  • $\begingroup$ @Andrej Thanks a lot for the hint. What I am mainly concerned about is that what causes, mandates, demands different $\beta$reduction steps to be equivalent in the language of category theory? Or if out another way, what does category theory have to say about $\beta$-equivalence? $\endgroup$
    – al pal
    Commented Nov 12, 2019 at 22:54
  • 1
    $\begingroup$ There's an old paper by Robert Seely in which he relates $\beta$-equivalences to 2-cells in a 2-category. This was a starting point for much further work, so if you look up who references that paper, you'll find a lot has been said about the question that interests you. $\endgroup$ Commented Nov 13, 2019 at 10:23


Your Answer

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