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

[Jon Sterling <jon@jonmsterling.com>]

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/21B50B02-4107-4854-8015-99EA4B14EBA5%40jonmsterling.com.