It depends on the representation. If $x,y:A\to X$ are morphisms in a category $C$, then the existence of an $f:X\to Y$ such that $f\circ x = y$ *can* be expressed in the internal language of $C$ itself. But that’s the “analytic” version where the “domain of variation” of a “variable quantity” is made explicit. For the implicit/synthetic version you have to work in a category of sheaves or something that builds in $A$, which means that *everything* you say in its internal language varies over $A$. So if $x,y:X$ in the internal language of this category-over-$A$, then if you write “there exists an $f:X\to Y$ such that $f(x)=y$” in *its* internal language, you get externally a statement in which $f$ also varies over $A$, i.e. a morphism $f:A\times X\to Y$, which is not what you want as the expected meaning of “$y$ is a function of $x$”.

Unfortunately my categorical logic notes don’t get this far yet. I found Part D of the Elephant to be a good place to learn about categorical logic in general, although it’s rather more encyclopedic than you may need. Also you can try the nLab, e.g. internal logic.

]]>I’ll report back if I get anywhere with this.

Related with the discussion over at MO here’s something I still don’t understand: why is it that the external property “There exists an $f:X\to Y$ such that $y=f\circ x$” is not something that can be expressed with the internal language of a topos/category? Probably I’ll need to study categorical logic and the “internal language of a topos” more thoroughly to understand the answer. I’ve tried reading the appendix in Anders Kock Synthetic differential geometry but had difficulties following it. Would your notes on categorical logic Mike cover the necessary topics to answer my question?

]]>Re #8, you could always direct to the nLab :) chain rule.

]]>For a while I dreamed of writing a calculus textbook based on this perspective. But eventually I decided that my calculus students, at least, suffer from much more basic problems than confusion about notation, and I should focus on addressing those to the extent I can.

I’ll be interested to see what you end up with.

]]>I see now that in your answer to the linked MO question you linked to Jason Howald’s question from 6 years ago, to which I today had added an answer essentially along the same lines as what you wrote there (involving a state space).

]]>Thanks Todd and Mike! In the meantime Mike also gave a very useful answer to my original question on MO, which leads me to conclude that STLC was probably not directly what I was looking for. The modal type theory Mike mentions over at MO seems more promising.

@Mike: in your longer answer at MO you asked me to elaborate what I was hoping to achieve with the example $y=x^2$. You seem to have understood the abuse of notation problem I was trying to explain. So I don’t know if this helps, but my ’original’ motivation for asking that MO question is that I’m dreaming of a proof checker for teaching (high-school) calculus the way it is actually used by physicist and engineers. (With variables, constants, “functions of” and a correct use of the notation dy/dx) This wish was ultimately sparked by your nforum thread “What is a variable?” from a few years ago.

]]>Yes, that’s right, sorry for using an unexplained abbreviation.

]]>Oh, maybe it’s “simply typed lambda calculus”?

]]>Thanks, Mike! That seems to be a good reference, but: what is STLC?

]]>One reference for the latter is section D4.2 in the Elephant.

]]>This would be the standard instance of simply typed $\lambda$-calculus generated by the finite-product theory of a ring object $R$ together with $f:R\to R \vdash D(f) : R\to R$ satisfying some axioms, right? So the question is just about where to find a proof that STLC generates free CCC’s?

]]>Over at MathOverflow, where the general discussion was on “logical foundations of variable-centric [high-school] calculus”, I had referred to an old $n$-Category Café discussion about this, and in my answer wrote

Categorical models of typed $\lambda$-calculus are cartesian closed categories, and the idea was to contemplate the universal (i.e., initial) cartesian closed category that comes equipped with

A commutative ring object $R$ (finite products suffice to describe what is meant by a commutative ring object),

A differentiation operator $D\colon R^R \to R^R$ (here $R^R$ is the “function space object” whose existence is given by cartesian closure; the elements of $R^R$ correspond to morphisms $R \to R$), satisfying all the formal expected properties of differentiation (product rule, chain rule, etc.).

This universal cartesian closed category can be constructed syntactically and could be called “the $\lambda$-theory of high school calculus”; I’ll call it $\mathit{Diff}$.

In a comment, Michael Bächtold wrote,” ’This universal cartesian closed category can be constructed syntactically’ Do you know if this has been written down somewhere? I just stumbled upon this, hoping to find an answer to my related question.” I don’t know a really good reference to give him. Can anyone help?

]]>