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$ – Andrej Bauer Nov 12 '19 at 20:50
  • $\begingroup$ @Andrej So you mean what it says on nLab is wrong? Or there is something I misunderstood? $\endgroup$ – al pal Nov 12 '19 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$ – Andrej Bauer Nov 12 '19 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 Nov 12 '19 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$ – Andrej Bauer Nov 13 '19 at 10:23

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.