0
$\begingroup$

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?!

Improve this question
$\endgroup$
5
  • 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, 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
    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$
    – Andrej Bauer
    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
    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$
    – Andrej Bauer
    Nov 13, 2019 at 10:23

0

Reset to default

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.