Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma 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 finite 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  1. 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.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2012
    • (edited Jul 5th 2012)

    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.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 5th 2012

    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.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2012
    • (edited Jul 5th 2012)

    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:XYf : X \to Y a differential dff D:X DY Dd 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.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 5th 2012

    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 DD of “infinitesimals”. The tangent bundle of a space XX is then defined as the exponential X DX^D, and it is a general fact having nothing to do with differentiation that the functor () D(-)^D can be equipped with the structure of a strong commutative monad. For example, the multiplication is defined as the composite

    (X D) DX D×DX ΔX D, (X^D)^D \simeq X^{D \times D} \stackrel{X^{\Delta}}{\to} X^D,

    where Δ:DD×D\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.”

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

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeJul 9th 2012

    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?

  3. 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 TT denote the set of trees. Let T 7T^7 denote the set of seven-tuples of trees. Let LL 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:TTs: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 7Tf:T^7\to T is defined by a pair ((p̲ i) iI,(q i) iI)((\underline p_i)_{i\in I},(q_i)_{i\in I}) of compatible substitutions:

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

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

    The application of ff to a 7-tuple t̲\underline t of trees is defined by: t̲s i(p i)\underline t\mapsto s_i(p_i) iff t̲\underline t is the unique instance (q̲ i,s i)(\underline q_i, s_i) of the 7-pattern q̲ i\underline q_i.

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

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJul 12th 2012

    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.