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

[Michael Shulman <shulman@sandiego.edu>]

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

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.



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

> Maybe just to put a finer point on it, re: the calculus example (and then
> I'll try to shut up, I have alreadyspoken too much):
>
> I subscribe to the viewpoint of the HoTT book regarding the practice of
> informal mathematics (or at least, I subscribe to a version of the
> viewpoint of the HoTT book which I think at least some of its authors held,
> including Steve Awodey with whom I have discussed this topic at length in
> the past). Things like terms, variables, and substitution do not actually
> arise in informal mathematics: instead, we work *directly* with things that
> are functions of other things. Thus when doing informal mathematics, if we
> say "term" we usually mean something that someone might more precisely
> refer to as an "element". (But let me not open that can of worms!)
>
> In that sense, it would be completely incorrect to say that when doing
> mathematics and we have a function `f(x) = x^2 + 1`, to evaluate f at 3 we
> must apply a syntactical operation that recursively walks a syntax tree and
> replaces a placeholder with 3. The function `f` has the same ontological
> status as a tree or as a friend or as a piece of stone: it is not a piece
> of code that tracks a function, rather it is *actually* a function --- in
> the same way that a stone is not a representation of an object, but an
> actual object. Thus to evaluate `f(3)`, we use what we know about `f`:
> namely that it is the function associated to the law that relates any
> number to the successor of its square.
>
> So in ordinary math, "substitution" tends to be a façon de parler for an
> operation that is not really syntactical at all but is instead
> intrinsically constitutive of the informal notion of a "mapping", which
> exists long before any logicians could attempt to intervene with their
> syntactical gesticulations... (By the way: truly syntactic substitution
> also arises *separately* in mathematics, by the way, when thinking about
> free extensions of algebraic objects (like rings of the form R[x]). But
> this is a very specialized usage, and if we are being precise we will
> always distinguish between an element of R[x] and the function it encodes.)
>
> It is true that it is possible to put aside this ontology, and think of
> mathematical objects in terms of their encodings and then make sure to only
> speak of syntactical operations that track mathematical operations (e.g.
> well-typed substitutions, but not ill-typed substitutions). But this is the
> way of logicians, and it is not really pertinent to the practice of
> everyday mathematics. Mathematics abstracts over these things, and we try
> to work "directly" with the objects we are concerned with, regardless of
> where we fall on the ancient debate of the "real-ness" of these objects.
>
> I fear we have veered off topic from the original question! But I think it
> would be great if we could put this debate to rest once and for all --- I
> am constantly amazed to be the syntactician in the room, but having
> semanticists insist to me that the study of syntax needs raw terms and
> variables and admissible substitution, etc. If it were needed, then I would
> certainly have noticed it by now! The world of syntax is far richer than
> can be described with mere trees or strings, and many of us who study
> syntax for a living have moved on from that viewpoint. ;-)
>
> Best,
> Jon
>
>
> On 18 Nov 2022, at 7:47, Jon Sterling wrote:
>
> > On 17 Nov 2022, at 21:35, Michael Shulman wrote:
> >
> >> As far as the mathematical study of type theories and their models goes,
> >> that may be true.  But I believe that when talking about the way type
> >> theories are used in practice, either on paper or in a proof assistant,
> >> there is still a difference.
> >>
> >> Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and
> I
> >> want to evaluate f(3).  I don't write
> >>
> >> f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.
> >>
> >> Instead, I jump right to f(3) = 3^2+1, because substitution is an
> operation
> >> that happens immediately in my head, not a computational step analogous
> to
> >> 3^2 = 9.  Similarly, the user of a proof assistant never types or sees
> >> substitution as part of the syntax; it is an operation *on* syntax that
> >> happens behind the scenes.
> >
> > By the way, I find this calculus example to be supremely uncompelling
> --- not because I am hung up on the fact that it pertains to a
> presentation, but because mathematics is full of equations that we
> basically agree not to mention at various times.
> >
> > It is also not particularly helpful to your point to bring up
> implementation, where it is extremely common to eschew implicit
> substitution for explicit substitutions --- or to use a mix of the two...
> In neither case are the details of this presented to the user, however,
> because the gender of an angel is not useful information to mere humans who
> use proof assistants.
> >
> > 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/CADYavpxMB%3D1kSPQM-OmSV_a9EauGmz7Gr-U3L%3DqfLCqsgzOnZQ%40mail.gmail.com.

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