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 definitions 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum 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.
   • CommentAuthorStephan A Spahn
   • CommentTimeJul 5th 2012
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItexI created [[types and calculus]] and [[seven trees in one]]. Both entries as yet contain just references. It would be nice to have more articles expanding on the reltion of calculus and (higher) category theory /type theory.

   I created types and calculus and seven trees in one. Both entries as yet contain just references.

   It would be nice to have more articles expanding on the reltion of calculus and (higher) category theory /type theory.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeJul 5th 2012
   • (edited Jul 5th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexMaybe the entry [[seven trees in one]] should have a pointer to Blass' article? And here is a general remark about editing strategy: I know that this is meant as a stub, but notice that your entry does not point to any other entry, is not pointed to from any other entry, has no Idea-section, has a title mysteriously unrelated to the two lines that it contains. Finally among those readers who will happen to come across it, few will even know what it _means_. So if you get run over by a bus tonight, this entry will with high probability be just lost. Nobody will find it. Nobody can even search for it, not even by chance. Do you see what I mean? My suggestion would be: even and in particular when creating a stub, try to provide some minimal context and interrelation so that the new entry becomes part of the nLab universe, and not just an isolated asteroid disconnected from everything else.

   Maybe the entry seven trees in one should have a pointer to Blass’ article?

   And here is a general remark about editing strategy: I know that this is meant as a stub, but notice that your entry does not point to any other entry, is not pointed to from any other entry, has no Idea-section, has a title mysteriously unrelated to the two lines that it contains. Finally among those readers who will happen to come across it, few will even know what it means.

   So if you get run over by a bus tonight, this entry will with high probability be just lost. Nobody will find it. Nobody can even search for it, not even by chance.

   Do you see what I mean? My suggestion would be: even and in particular when creating a stub, try to provide some minimal context and interrelation so that the new entry becomes part of the nLab universe, and not just an isolated asteroid disconnected from everything else.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeJul 5th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThere's that work on generalized species, e.g., [The cartesian closed bicategory of generalised species of structures](http://www.cs.le.ac.uk/people/ngambino/Publications/generalised-species.pdf), which forms a model of Ehrhard and Regnier's [Differential Lambda-Calculus](http://www.pps.univ-paris-diderot.fr/~ehrhard/pub/difflamb.pdf). >...the bicategory of generalised species provides also a 2-dimensional model of both the typed and the untyped differential lambda calculus. Hmm, if Lambek and Scott cover: typed and untyped $\lambda$-calculus and then type theory, modelled by cartesian closed categories and toposes, and if we're all getting excited about homotopizing and then cohesifying type theory, could we have done the same to the $\lambda$-calculus, and, if so, would it bear any relation to Ehrhard and Regnier? Apparently, there's [discussion](http://arxiv.org/abs/1202.0411) of the best categorical models of the Differential Lambda-Calculus, whether cartesian differential categories or differential $\lambda$-categories.

   There’s that work on generalized species, e.g., The cartesian closed bicategory of generalised species of structures, which forms a model of Ehrhard and Regnier’s Differential Lambda-Calculus.

   …the bicategory of generalised species provides also a 2-dimensional model of both the typed and the untyped differential lambda calculus.

   Hmm, if Lambek and Scott cover: typed and untyped $\lambda$-calculus and then type theory, modelled by cartesian closed categories and toposes, and if we’re all getting excited about homotopizing and then cohesifying type theory, could we have done the same to the $\lambda$-calculus, and, if so, would it bear any relation to Ehrhard and Regnier?

   Apparently, there’s discussion of the best categorical models of the Differential Lambda-Calculus, whether cartesian differential categories or differential $\lambda$-categories.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeJul 5th 2012
   • (edited Jul 5th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexGood question. I am unlikely to have time to look into this. But: how is this not covered by Lawever's notion of synthetic differential geometry? You can think of his axioms as being precisely such as to be able to assign to every term of function type $f : X \to Y$ a differential $d f \coloneqq f^D : X^D \to Y^D$ obtained by homming the infinitesimally extended point into it. The homotopy-fication of this is [[infinitesimal cohesion]].

   Good question.

   I am unlikely to have time to look into this. But: how is this not covered by Lawever’s notion of synthetic differential geometry? You can think of his axioms as being precisely such as to be able to assign to every term of function type $f : X \to Y$ a differential $d f \coloneqq f^D : X^D \to Y^D$ obtained by homming the infinitesimally extended point into it.

   The homotopy-fication of this is infinitesimal cohesion.

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeJul 5th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI see Manzyuk [writes](http://arxiv.org/abs/1202.0411): "For readers familiar with synthetic differential geometry [11], it should not come as a surprise that the tangent bundle functor is part of a strong commutative monad. Indeed, synthetic differential geometry is developed relative to a topos that is assumed to contain an object $D$ of "infinitesimals". The tangent bundle of a space $X$ is then defined as the exponential $X^D$, and it is a general fact having nothing to do with differentiation that the functor $(-)^D$ can be equipped with the structure of a strong commutative monad. For example, the multiplication is defined as the composite $$ (X^D)^D \simeq X^{D \times D} \stackrel{X^{\Delta}}{\to} X^D, $$ where $\Delta: D \to D \times D$ is the diagonal morphism. However, we still think that the results presented in this note are of some interest, as they operate at a more basic level. Topoi enjoy many powerful properties. In contrast, the notion of tangent bundle and its associated algebraic structures make sense in any cartesian differential category, which is a minimal setup in which differential calculus and other notions reminiscent of it can be described. Differentiation appears in different guises in both combinatorics and computer science."

   I see Manzyuk writes:

   “For readers familiar with synthetic differential geometry [11], it should not come as a surprise that the tangent bundle functor is part of a strong commutative monad. Indeed, synthetic differential geometry is developed relative to a topos that is assumed to contain an object $D$ of “infinitesimals”. The tangent bundle of a space $X$ is then defined as the exponential $X^D$, and it is a general fact having nothing to do with differentiation that the functor $(-)^D$ can be equipped with the structure of a strong commutative monad. For example, the multiplication is defined as the composite

   $$(X^D)^D \simeq X^{D \times D} \stackrel{X^{\Delta}}{\to} X^D,$$

   where $\Delta: D \to D \times D$ is the diagonal morphism. However, we still think that the results presented in this note are of some interest, as they operate at a more basic level. Topoi enjoy many powerful properties. In contrast, the notion of tangent bundle and its associated algebraic structures make sense in any cartesian differential category, which is a minimal setup in which differential calculus and other notions reminiscent of it can be described. Differentiation appears in different guises in both combinatorics and computer science.”

6. • CommentRowNumber6.
   • CommentAuthorStephan A Spahn
   • CommentTimeJul 5th 2012
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItex> And here is a general remark about editing strategy: Sorry, I planned to return to the article later on and add these things - what I have done by now. > So if you get run over by a bus tonight, this entry will with high probability be just lost. Yes, in any case it is good to have the possible consequences of such unwise doing as leaving an article in a dangling state described with such urgency;)

   And here is a general remark about editing strategy:

   Sorry, I planned to return to the article later on and add these things - what I have done by now.

   So if you get run over by a bus tonight, this entry will with high probability be just lost.

   Yes, in any case it is good to have the possible consequences of such unwise doing as leaving an article in a dangling state described with such urgency;)

7. • CommentRowNumber7.
   • CommentAuthorTobyBartels
   • CommentTimeJul 9th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex>There is a bijection between the set of finite binary trees and the set of seven-tuples of such. This is trivial; both sets are countably infinite. I changed ‘bijection’ to ‘natural bijection’, but I don't actually know what this means. What are the functors involved?

   There is a bijection between the set of finite binary trees and the set of seven-tuples of such.

   This is trivial; both sets are countably infinite. I changed ‘bijection’ to ‘natural bijection’, but I don’t actually know what this means. What are the functors involved?

8. • CommentRowNumber8.
   • CommentAuthorStephan A Spahn
   • CommentTimeJul 10th 2012
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItexIn the paper ''seven trees in one'' the bijections of interest are called ''very explicit bijections''. This notion is defined there as follows: Let *tree* mean finite binary tree. Let $T$ denote the set of trees. Let $T^7$ denote the set of seven-tuples of trees. Let $L$ be a finite set of ''labels''. A *pattern* is defined to be a tree possessing some leaves which are labelled by distinct labels. A *7-pattern* is defined to be a seven tuple of patterns whose labels are all distinct. A *substitution* is defined to be a function $s:T\to T$ substituting a label by some tree. An *instance* is defined to be a value of some pattern under some substitution. A substitution of a 7-pattern is defined analogously. An *very explicit function $f:T^7\to T$* is defined by a pair $((\underline p_i)_{i\in I},(q_i)_{i\in I})$ of *compatible substitutions*: 1. $(\underline p_i)_{i\in I}$ is a set of 7-patterns such that every 7-tuple of trees $\underline t$ is an is an instance $(\underline p_i,s_i)$ of precisely one $\underline p_i$ under precisely one substitution $s_i$. 1. $(q_i)_{i\in I}$ is a set of patterns (indexed by the same $I$) such that $q_i$ has the same labels as $\underline p_i$ The application of $f$ to a 7-tuple $\underline t$ of trees is defined by: $\underline t\mapsto s_i(p_i)$ iff $\underline t$ is the unique instance $(\underline q_i, s_i)$ of the 7-pattern $\underline q_i$.

   In the paper ”seven trees in one” the bijections of interest are called ”very explicit bijections”. This notion is defined there as follows:

   Let tree mean finite binary tree. Let $T$ denote the set of trees. Let $T^7$ denote the set of seven-tuples of trees. Let $L$ be a finite set of ”labels”.

   A pattern is defined to be a tree possessing some leaves which are labelled by distinct labels. A 7-pattern is defined to be a seven tuple of patterns whose labels are all distinct.

   A substitution is defined to be a function $s:T\to T$ substituting a label by some tree. An instance is defined to be a value of some pattern under some substitution. A substitution of a 7-pattern is defined analogously.

   An very explicit function $f:T^7\to T$ is defined by a pair $((\underline p_i)_{i\in I},(q_i)_{i\in I})$ of compatible substitutions:

   1. $(\underline p_i)_{i\in I}$ is a set of 7-patterns such that every 7-tuple of trees $\underline t$ is an is an instance $(\underline p_i,s_i)$ of precisely one $\underline p_i$ under precisely one substitution $s_i$.

   2. $(q_i)_{i\in I}$ is a set of patterns (indexed by the same $I$) such that $q_i$ has the same labels as $\underline p_i$

   The application of $f$ to a 7-tuple $\underline t$ of trees is defined by: $\underline t\mapsto s_i(p_i)$ iff $\underline t$ is the unique instance $(\underline q_i, s_i)$ of the 7-pattern $\underline q_i$.

9. • CommentRowNumber9.
   • CommentAuthorStephan A Spahn
   • CommentTimeJul 10th 2012
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItexThe matter of functoriality of this construction is addressed in that paper, too, I guess. But I didn't yet find the time to extract it.

   The matter of functoriality of this construction is addressed in that paper, too, I guess. But I didn’t yet find the time to extract it.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJul 12th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> if we're all getting excited about homotopizing and then cohesifying type theory, could we have done the same to the λ-calculus? Well, typed $\lambda$-calculus is just part of type theory, so that's already done. I don't have any idea what it would mean to homotopify *untyped* $\lambda$-calculus, but it's an intriguing idea.

    if we’re all getting excited about homotopizing and then cohesifying type theory, could we have done the same to the λ-calculus?

    Well, typed $\lambda$-calculus is just part of type theory, so that’s already done. I don’t have any idea what it would mean to homotopify untyped $\lambda$-calculus, but it’s an intriguing idea.