Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman <shulman@sandiego.edu>]

[-- Attachment #1: Type: text/plain, Size: 6232 bytes --]

Thanks.  It does sound like we mostly agree.  I would probably argue that
even for type theories in development, where we don't yet know that full
definitional equality is decidable -- or intrinsically ill-behaved type
theories like Lean, or Agda with non-confluent rewrite rules, where
definitional equality *isn't* decidable -- there is still value in being
able to reduce just substitutions.  But I think that's a relatively minor
point.

Maybe we can work out some way to use words so that this underlying
agreement is evident.  For instance, can we find a third word to use
alongside "admissible" and "derivable" to refer to operations/equalities
like substitution and its theory, which hold in all reasonable models, and
can be made admissible in some presentations, but more importantly can be
eliminated in an equality-checking algorithm?


On Fri, Nov 18, 2022 at 8:38 AM Jon Sterling <jon@jonmsterling.com> wrote:

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

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxB3-n6Udm86ZDZQTKUTYfgzjHWM6g85_-ANpo6pVsOqQ%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 7171 bytes --]