Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 12th 2018
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexOver at [MathOverflow](https://mathoverflow.net/a/115667/2926), 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](https://mathoverflow.net/q/307947/745)." I don't know a really good reference to give him. Can anyone help?

   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?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeAug 12th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThis 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?

   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?

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeAug 12th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOne reference for the latter is section D4.2 in the [[Elephant]].

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

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 12th 2018
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks, Mike! That seems to be a good reference, but: what is STLC?

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

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 12th 2018
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexOh, maybe it's "simply typed lambda calculus"?

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

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeAug 12th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYes, that's right, sorry for using an unexplained abbreviation.

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

7. • CommentRowNumber7.
   • CommentAuthorMichael_Bachtold
   • CommentTimeAug 13th 2018
   • (edited Aug 13th 2018)
   • PermaLink
   Author: Michael_Bachtold
   Format: MarkdownItexThanks 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](https://mathoverflow.net/q/115416/745)) This wish was ultimately sparked by your nforum thread "What is a variable?" from a few years ago.

   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.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeAug 13th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI see now that in your answer to the linked MO question you linked to Jason Howald's [question](https://mathoverflow.net/q/84221/49) 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).

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

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeAug 13th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexFor 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.

   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.

10. • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 13th 2018
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRe #8, you could always direct to the nLab :) [[chain rule]].

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

11. • CommentRowNumber11.
    • CommentAuthorMichael_Bachtold
    • CommentTimeAug 14th 2018
    • (edited Aug 14th 2018)
    • PermaLink
    Author: Michael_Bachtold
    Format: MarkdownItexI'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?

    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?

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeAug 14th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIt 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]].

    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.