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.
1 to 7 of 7
I just noticed that the Isbell envelope $E(\mathcal{T})$ embeds fully-faithfully into the Chu construction $Chu(Set^{\mathcal{T}^{op}\times\mathcal{T}},\hom_{\mathcal{T}})$. An object of the latter consists of two endo-profunctors $P,F : \mathcal{T}^{op}\times\mathcal{T}\to Set$ together with a natural transformation $P\times F \to \hom_{\mathcal{T}}$, and the image of $E (\mathcal{T})$ consists of those triples such that $P$ depends only on $\mathcal{T}^{op}$ and $F$ depends only on $\mathcal{T}$. Does this mean anything? Is it good for anything?
Stumbling upon this on a Sunday morning wander, we talk about duality in an Isbell context (Isbell envelope, Isbell duality) and in a Chu context (Chu construction), but without relating them. Isbell pages don’t mention ’Chu’, and vice versa.
It seems (Linear Logic for Constructive Mathematics) that the Chu outlook is good for setting constructions in terms of linear logic, so might we expect that it could be used to formulate that work on linear HoTT? If Chu constructions act interestingly on toposes of various kinds (Heyting algebras, etc), then why not on $(\infty, 1)$-toposes?
How about a $Chu((\infty, 1)$-topos, object classifier)? That would seem to take us in a integral transforms on sheaves direction, with a fibration over a product as an integral kernel.
It’s a bit funny: the “prototypical” Chu construction on a 1-category is $Chu(Set,Prop)$ (Chu spaces), which as you say categorifies to $Chu(\infty Gpd, \infty gpd)$. But since (-2)-categories are trivial, its obvious decategorification would be $Chu(Prop,1)$, whereas in LLCM I used instead $Chu(Prop,0)$. The latter also categorifies to $Chu(Set,0)$ and $Chu(\infty Gpd,0)$. And any of these can be done “fibered” over the base DTT for $Set$ or $\infty Gpd$, producing a model of dependent linear type theory with linear types depending on nonlinear ones; the fibered $Chu(Set,0)$ appears briefly in Remark 9.12 of LLCM.
There’s another construction that “combines the idea of a category of presheaves with that of the Chu construction” in Hyland’s Proof theory in the abstract, section 5, called the “envelope of a polycategory”.
So if the $Chu(n Gpd, 0)$ family corresponds to a linear type theory, how would one describe the object classifier family? It would seem to include a groupoidified linear algebra.
All Chu constructions are $\ast$-autonomous and hence have a linear type theory.
1 to 7 of 7