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(𝒯) embeds fully-faithfully into the Chu construction Chu(Set𝒯op×𝒯,hom𝒯). An object of the latter consists of two endo-profunctors P,F:𝒯op×𝒯→Set together with a natural transformation P×F→hom𝒯, and the image of E(𝒯) consists of those triples such that P depends only on 𝒯op and F depends only on 𝒯. 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 (∞,1)-toposes?
How about a Chu((∞,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(∞Gpd,∞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(∞Gpd,0). And any of these can be done “fibered” over the base DTT for Set or ∞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(nGpd,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 *-autonomous and hence have a linear type theory.
1 to 7 of 7