Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
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.
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.
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.”
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;)
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?
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:
$(\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$.
$(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$.
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.
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.
1 to 10 of 10