MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Consider two contexts $\Gamma,\Delta$ (from some background type theory), and substitutions $s_1,s_2:\Gamma\rightarrow \Delta$. In the case of $1$-element contexts, we get that a substitution is simply a term in the $\lambda$-calculus; in that case, we know that the 'natural' relations between terms arise from $\beta$-reduction (and sometimes $\eta$-contraction, $\delta$-convertibility and $\alpha$-renaming). For example, Robert Seely conjectured [that article claims a proof, but a full proof only came many years later] that if the contexts belong from some dependently typed theory, there is a correspondance with locally cartesian closed categories, where the $2$-cells are given exactly by rewrites engendered by $\beta$ and $\eta$.

My question is, in general, what are the general relations which are considered natural between substitutions $s_1,s_2:\Gamma\rightarrow\Delta$ ?

Since the category of contexts is the opposite of the category of theory presentations, it is fairly natural to conjecture that this will be related to morphisms of theory interpretations. So, looking at $2$-categories as CAT-enriched categories, one finds some work on categories of interpretations, but it is not clear to me that this is indeed the right direction to look into.

In particular (from my admittedly CS-biased point-of-view), I would have expected something which more closely resembles term-rewriting in some guise. But maybe I am simply not recognizing that what is given above is a semantic counterpart to something more operational.

share|cite|improve this question

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.