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

[Jon Sterling <jon@jonmsterling.com>]

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/9B3B568C-452A-4919-A149-CF7C1E91CDAE%40jonmsterling.com.