Hi Mike,

Thanks for this! I think we are getting a lot closer.

On 18 Nov 2022, at 11:25, Michael Shulman wrote:

> In general, I feel like we are still talking past each other.  Maybe the
> problem is that I still haven't found the words that will communicate my
> point to you.  I was trying to say that it isn't the word "admissible" that
> matters, but there are real mathematical questions going on whatever words
> you use to talk about them.
>
> Last summer when I was explaining something about HOTT to a group that I
> think included you, I used the phrase "admissible" for a certain equality,
> and we got into a bit of this discussion.  But I felt like we agreed in the
> end that what I meant was "a rule that doesn't have to get used explicitly
> by the conversion-checker", and that it was useful to distinguish such
> things whatever we call them.  That's what I was trying to get at with
> "rules that hold in all models and can be made to hold in a particular
> presentation of the free model without being given explicitly as generating
> operations/equalities".
>
> Similarly, I don't think the implicitness or explicitness of substitutions
> in the syntax is what's crucial.  If you formulate substitutions
> implicitly, then the statement you want is that substitution can be defined
> as an "admissible" operation on the syntax.  If you formulate substitutions
> explicitly, then the statement you want is that substitutions can be
> eliminated by a computation.  Isn't this what you mean by "The equational
> theory of substitution in this situation (particularly, how to commute
> substitutions past the modal forms) is the hard part"?  You don't just want
> an equational theory for substitution -- the equations in an equational
> theory are undirected -- but some kind of rewriting system that tells you
> how to push a substitution inside the modal forms.  Whether the
> substitutions are part of the syntax or not isn't the point.
>

I agree with a lot of what you have written here, but maybe not all of it. Let me put it my own way, which is probably similar to what you are getting at --- I see deciding the equational theory of substitution as a special case of deciding the rest of the equational theory. To me, it is basically useless to have a decision procedure for "reducing substitutions but not any other computations (like beta laws, etc.)". To put it another way, if I don't have an algorithm for full normalization (or at least deciding def.eq.), I really couldn't care less if I have an algorithm for reducing substitutions.

Regarding things that exist in the syntax but not necessarily in all models, this is indeed the point of admissibility and it's really really important! It just so happens, however, that substitutions are the main example of something that is both admissible **and** exists in all reasonable models. Even in weak models, we have substitution up to isomorphism --- and no existing solution to the Seely substitution coherence problem works by saying "Well, substitution is admissible, so we don't need it in the model anyway". So the one place to look for an example of substitution-admissibility being important in type theory is actually a non-example.

Not all admissible rules are as useless as this! To the contrary, there ARE very important examples of different admissible rules that must not be derivable unless we wish to degenerate the theory; the main examples that have practical import are injectivity laws, which allow you to deterministically reduce complex equality problems to simpler ones; without these, elaboration and type checking would be essentially impossible (whereas elaboration and typechecking are completely insensitive to the question of whether substitution is admissible). Injectivity of type constructors is the main example of an important admissible rule, but there are many more examples (and I expect, based on our conversations about HOTT over the summer) that there will be a lot more interesting and important ones to discover in the coming years.

So in case it clarifies me, I think admissibility is extremely important and it is, in some sense, the main topic that people like me study. My experience has led me, however, to make a distinction between admissibilities that matter (like injectivity laws) and ones that do not matter at all (like substitution). Nonetheless, there are many roads to the same idea, and the study of type theory and logic in terms of admissible substitutions has been (and remains) an extremely reliable and effective way to obtain well-behaved theories. All I am doing is trying to tease out which parts of this process were essential, and which parts were incidental.

Best,
Jon