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

Discussion Tag Cloud

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).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeDec 7th 2013
    • (edited Dec 7th 2013)

    When considering pull-push in generalized cohomology as six-operations yoga in E E_\infty-geometry, then one runs into the following structure, and I am wondering if this has an established name and has been studied before:

    First, there is the evident “many-object version” of a monad, does this have an established name? A “monad-oid”? I mean a system of categories with chosen functors betweem any pair of them and equipped with composition transformations from any two consecutive ones to the one from the leftmost domain to the rightmost codomain, satisfying associativity and unitalness in the evident way.

    Then given a “monad-oid” like this, there is an evident oid-y Kleisli category: objects are objects in any of the above categories, morphisms are morphisms from one object to the image of the other under the relevant functor, and composition is defined using the above composition transformations. Does this have an established name and has this been studied before?

    In themselves these are straightforward extensions of the notion of monad and Kleisli category, I am just trying to feel my way into how to best look at the situation that I am considering and so I am wondering if this oid-y Kleisli situation has maybe elsewhere been found to be of independent value.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2013

    Benabou called it a “polyad”. Nowadays it’s more commonly called a “category enriched in a bicategory”. Richard Garner and I recently wrote about them (read the introduction and then skip to section 15).

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 7th 2013

    You point out another instance of the microcosm principle:

    the proper context in which to consider the theory of enriched categories is a categorified version of itself.

    Ought the principle as written be extended:

    Certain algebraic structures can be defined in any category equipped with a categorified version of the same structure,

    as here things are being defined in bicategories equipped with something?

    And is more known yet about

    The microcosm principle is a general heuristic, but in some contexts, a general version of it can be proven formally?

    E.g., are there places where you might expect it to work but it doesn’t?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeDec 7th 2013
    • (edited Dec 7th 2013)

    Ah, right, enriched in a bicategory. Thanks.

    I see “Kleisli” appear in your article, but is it related to the many-object version of the Kleisli catgeory of a monad?

    So for instance suppose we have two functors

    𝒞 1F 1𝒞 2F 2𝒞 3 \mathcal{C}_1 \stackrel{F_1}{\leftarrow} \mathcal{C}_2 \stackrel{F_2}{\leftarrow} \mathcal{C}_3

    and a composition c:F 1F 2F 3c \colon F_1 \circ F_2 \Rightarrow F_3

    then I’d be looking for the category where a morphism for instance from A 1𝒞 1A_1 \in \mathcal{C}_1 to A 2𝒞 2A_2 \in \mathcal{C}_2 is a morphism in 𝒞 1\mathcal{C}_1 of the form f 1:A 1F 1(A 2)f_1 \colon A_1 \to F_1(A_2) and composition of this with a morphism from A 2A_2 to A 3𝒞 3A_3 \in \mathcal{C}_3 given by some f 2:A 2F 2(A 3)f_2 \colon A_2 \to F_2(A_3) would be

    A 1f 1F 1(A 2)F 1(f 2)F 1(F 2(A 3))c(A 3)F 3(A 3). A_1 \stackrel{f_1}{\longrightarrow} F_1(A_2) \stackrel{F_1(f_2)}{\longrightarrow} F_1(F_2(A_3)) \stackrel{c(A_3)}{\longrightarrow} F_3(A_3) \,.

    (I know you know what I mean, this here just for definiteness to have something to point to.)

    What would this construction be thought of in the context of bicategory enrichment?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2013

    @Urs: we call it the “collage” after Street; see 15.9 for the abstract definition, and the second paragraph of 16.19 for a mention of how when interpreted in Cat it gives what you are describing.

    @David: I always understood “category” in the microcosm principle as referring also to higher categories.

    • CommentRowNumber6.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 8th 2013

    Certain algebraic structures can be defined in any category equipped with a categorified version of the same structure,

    Are you thinking of doctrines, David? As in monoids can be defined in a monoidal category etc?

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 8th 2013

    That is taken from the microcosm principle page. I was just wondering if we needed something like

    Certain higher algebraic structures can be defined in any higher category equipped with a categorified version of the same structure,

    but Mike’s reassured me we can take the ’higher’s as read.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeDec 8th 2013
    • (edited Dec 8th 2013)

    David C., but the page microcosm principle is very explicit on this, isn’t it? I started the page when it struck me how Lurie’s discussion of higher algebra is all based on a formalization of the microcosm principle in \infty-operad theory.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 8th 2013

    Isn’t Lurie talking about (,1)(\infty, 1) while Mike’s example is (2,2)(2, 2)?

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 8th 2013
    • (edited Dec 8th 2013)

    Mike, thanks for the further pointers! That helps, now I see it in your article.

    (I added a pointer to this at Kleisli object, don’t want to mess with collage right now (and why not stick with “Kleisli object” also for the many-object case?). Have also split off a brief category enriched in a bicategory from enriched category, just for completeness; cross-linked briefly with proarrow equipment.)

    Okay, now I can begin to see if your result helps in the application that I am looking at.

    What I am looking at is closely related to your other article “Enriched indexed categories”. I suppose the enriching bicategory 𝒞\mathcal{C} is to be taken to be something like MonCatMonCat maybe, or some completion thereof (not sure) and the 𝒞\mathcal{C}-enriched categories of interest are categories AA whose objects’ extent lands in objects of Fam(𝒱)Fam(\mathcal{V}) for some closed monoidal 𝒱\mathcal{V}, and whose morphisms are pull-push (p 1) !(p 2) *(p_1)_! (p_2)^\ast through spans of morphisms in Fam(𝒱)Fam(\mathcal{V}) that satisfy Beck-Chevalley.

    As you see, this is a very classical setup and possibly what I am looking for is also already classical. Maybe all I am really asking is: what would be the modern perspective in view of indexed closed monoidal categories of six-operations yoga in Wirthmüller flavor?

    But specifically I am interested in the Kleisli objects/collages of such yoga, which is maybe not discussed classically in this context, not sure.

    Now theorem 1.6 in your article with Garner somehow says that if I want all the corresponding Kleisi objects/collages to exist nicely, I should pass to 𝒞\mathcal{C}-enriched categories with 𝒞\mathcal{C}-enriched profunctors/modules between them. I need to think about what this is really telling me in the given application…

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 8th 2013

    I am still thinking about your specific question in the other thread. Do you mean anything more general than that question by “collages of yoga”?

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 8th 2013
    • (edited Dec 8th 2013)

    Right, I should give a more coherent account of what I am looking at and asking about.

    I have made a quick note on that with more details here:

    • Abstract integral transforms (pdf)

    Motivation:

    The operation of pull-push of quasi-coherent sheaves of modules through correspondences embodies some higher analog of matrix calculus and more generally of the theory of integral transformations via integral kernels \cite{BZ08}; the seminal historical example being the Fourier-Mukai transform. On the other hand, another higher analog of integral transform theory is given by pull-push in generalized twisted cohomology (twisted Umkehr maps \cite{ABG11}), as it appears for instance in the construction of string topology operations and in the discussion of T-duality. What has apparently been lacking (?) is the identification of a core general abstract framework for integral transforms that would make both these applications be special cases in a way that their main properties follow formally from general statements.

    At least a central ingredient of such a formalization should be a “yoga of six operations” that Grothendieck famously identified as the abstract mechanism underlying Grothendieck-Verdier duality. A clean analysis of the possible flavors of this six-operations axiomatics and their corresponding implications has been given in \cite{May05}. The central formal consequence highlighted there is the “Wirthmüller isomorphism” which says, when it applies, that pull-push respects dualization, up to, possibly, a certain natural twist.

    We observe below, in exmaple \ref{PullPushInGeneralizedCohomology} following \cite{Nuiten13}, that it is precisely this statement which also formally controls the twisted Umkehr maps in generalized cohomology theory \cite{ABG11}, using that these Umkehr maps are built by first dualizing (Poincaré duality), then pushing, then dualizing back, possibly picking up a twist thereby.

    Motivated by this example, in this note we are after identifying a general abstract (higher) algebraic formalization of integral kernels and integral transformations.

    Specifically we are after a formalization that may mesh well with axiomatic cohesion. In the context of axiomatic cohesion one regards the ambient category of spaces and (principal) bundles over them as forming an indexed cartesian closed monoidal category equipped with a system (a “yoga”) of base change morphisms (hyperdoctrine) and equipped with some monads used to express the intended modalities characterizing such spaces. Below it turns out that we are working essentially in a linear monoidal (“tensor”) or “quantum” variant of this setup, where instead of an indexed topos we have an indexed closed monoidal linear category (as in \cite{Shulman12}, theorem 2.14). As for axiomatic cohesion we find that the yoga of adjoint base change functors becomes most natural and transparent when expressed in terms of (just) the (co-)monads induced by these adjunctions.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeDec 8th 2013

    Okay, I think I see what you’re doing, at least. It’s not obvious to me that you want to be in a bicategory of monoidal categories; colimits therein would generally involve some sort of free cocompletion under monoidal products. Are you expecting the collage (the category whose morphisms are the integral kernels) to be again a monoidal category? It seems more likely to me that you’re just looking at a collage in CatCat which happens to be constructed using monoidal structures on some particular categories. And collages in Cat are already nice and well-behaved and give you the Kleisli-like composition you’re seeing. This has the additional advantage that you can take collages when the morphisms are profunctors and not just functors, which seems to me may be necessary to take account of the twisting objects.

    • CommentRowNumber14.
    • CommentAuthorzskoda
    • CommentTimeDec 8th 2013
    • (edited Dec 8th 2013)

    12 You might want to consult

    • Alexander Polishchuk, Kernel algebras and generalized Fourier-Mukai transforms, arxiv/0810.1542

    for some relevant related ideas.

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2013

    In the context of axiomatic cohesion one regards the ambient category of spaces and (principal) bundles over them as forming an indexed cartesian closed monoidal category equipped with a system (a “yoga”) of base change morphisms (hyperdoctrine) and equipped with some monads used to express the intended modalities characterizing such spaces.

    I hadn’t made the connection with that work I discussed once on modal hyperdoctrines. That was part of an extended Stone duality for modal logic.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2013
    • (edited Dec 9th 2013)

    Thanks for all the replies! I’ll briefly react to them here, but will have to postpone more detailed reactions until tomorrow.

    @Mike: Thanks, good point, yes, maybe staying in CatCat is what I need. And, true, I ignored the twists so far when asking for the Kleisli category picture, for simplicity. I suppose I should throw them over to the other side of the morphisms anyway, I need to think more about this.

    @Zoran, thanks for the pointer to Polishchuk! That article considers integral transforms in the “Grothendieck context” (and I have added a pointer in the References-section there now). I have focused on the dual “Wirthmüller context” for the time being, since that most directly includes the pull-push in twisted generalized cohomology. But somehow all this should have a dual description in “Grothendieck contexts”, I suppose. I was talking about this with Joost. But I need to look into this more.

    @David, yes, so dependent type theory with idempotent (co-)monads is an implementation of “modal hyperdoctrines”, if you wish. I tend to avoid the word “hyperdoctrine” here since it makes something very elementary and basic sound like a big deal. But now that we are passing from indexed cartesian closed contexts to indexed linear monoidal (tensor) closed contexts, it maybe helps to highlight what’s going on.

    So “before quantization” we associate to morphisms f:XYf : X \to Y base change adjoint triples ( ff * f)(\sum_f \dashv f^\ast \dashv \prod_f) between toposes, being dependent sum, context extension, dependent product. Now “when quantizing” we instead associate to morphisms f:XYf : X \to Y base change adjoint triples (f !f *f *)(f_! \dashv f^\ast \dashv f_\ast) between closed tensor categories that constitute “Wirthmüller contexts” (Frobenius reciprocity). Clearly there is at least a strong analogy here and that’s part of the motivation for exploring the formal consequences of the latter further.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2013
    • (edited Dec 9th 2013)

    Gr, somehow I keep thinking more about this issue here than about what I am supposed to be working on today.

    Maybe to come back to David’s comment above, the thoughts that now keep haunting me go like this (copied from a post shared elsewhere):


    Grothendieck’s Yoga of Six-Operations and some Quantum Dependent Type Theory?

    Grothendieck had famously amplified that the mechanism of Verdier duality is formally captured by certain systems of adjoint pairs of functors – the “yoga of six operations”:

    http://ncatlab.org/nlab/show/six+operations .

    A clean analysis of these axioms and their consequences had been given by Peter May, who highlights that flavor of the axioms that he calls the “Wirthmüller context”:

    http://ncatlab.org/nlab/show/Wirthmüller+context

    A Wirthmüller context is simply this: an adjoint triple of functors between two closed monoidal categories such that the middle one is strong closed monoidal, hence such that Frobenius reciprocity holds:

    http://ncatlab.org/nlab/show/Frobenius+reciprocity .

    If in addition a Beck-Chevalley condition holds for consecutive such Wirthmüller morphisms

    http://ncatlab.org/nlab/show/Beck-Chevalley+condition

    then there is canonically induced an abstract calculus of integral transforms via integral kernels that captures a great deal of genuine quantum physics:

    https://dl.dropboxusercontent.com/u/12630719/integral.pdf

    notably it captures geometric quantization of symplectic manifolds, of Poisson manifolds, of Wilson loops, the quantization of strings, T-duality, D-brane charge,…, all via example 3.5 of the above note, which establishes the dictionary and then points you to

    http://ncatlab.org/schreiber/show/master+thesis+Nuiten

    for the details of the implementation.

    But now for the special case that the monoidal categories in the Wirthmüller context are cartesian all this

    1. triple of adjoint functors

    2. the middle one is strong closed monoidal, hence satisfies Frobenius reciprocity

    3. Beck-Chevalley condition holds

    are Lawvere’s axioms on categorical logic

    http://ncatlab.org/nlab/show/hyperdoctrine

    The well behaved examples of this arise from base change of slice toposes. Indeed, given any topos, then its dependent type theory

    http://ncatlab.org/nlab/show/dependent+type+theory

    is a system of cartesian Wirthmüller six-operation contexts, the left adjoints being dependent sum, the middle functors being context extension, and the right adjoints being dependent products.

    In other words: Grothendieck’s six operation yoga in Wirthmüller flavor is a non-cartesian variant of core aspects of dependent type theory.

    In particular, if the closed monoidal categories here are “linear”, hence are “tensor categories”, then this is a “linear” or “quantum” analog of key ingredients in dependent type theory.

    Does this resonate with anyone?

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2013

    What happens when homotopy type theory meets linear logic? I see “linear type theory” has some hits. Even “linear dependent type theory” does.

    The other way – “dependent linear type theory” – sends us to our own page dependent sum type:

    One might expect that in “dependent linear type theory” the positive and negative dependent sums would become different. However, the meaning of the quoted phrase is unclear.

    Also it seems to

    S.S. Ishtiaq and D. J. Pym. A relevant analysis of natural deduction. Journal of Logic and Computation, 8(6):809–838, 1998. (pdf).

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeDec 9th 2013

    What happens when homotopy type theory meets linear logic?

    The best way I’ve thought of so far to combine DTT with LTT is to have two classes of types, “linear” and “nonlinear”, where the nonlinear ones form an ordinary DTT and the linear types can depend on nonlinear types, but not on each other. There’s been some work on stuff like this from the type-theoretic side, but not I think a whole lot. Semantically, this models an indexed monoidal category (the linear types) over a cartesian base (the nonlinear ones).

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2013

    Mike, that sounds just like what I would like to see (a propos: a tangent \infty-topos is already a lot like this, only that one still needs to add the tensor product). Where is more on this written up, if anywhere?

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2013
    • (edited Dec 9th 2013)

    In

    • Paul-André Melliès , Categorial Semantics of Linear Logic, in Interactive models of computation and program behaviour, Panoramas et synthèses 27, 2009 (pdf)

    and

    • Andrew Graham Barber, around p. 21 of Linear Type Theories, Semantics and Action Calculi, 1997 (web, pdf)

    the !!-modality is interpreted as the comonad induced from a monoidal adjunction between a cartesian and the symmetric monoidal (star-autonomous) type system.

    Viewed from the point of view of tangent \infty-toposes, maybe the canonical choice for the monoidal

    CartesianMonoidalSymmetricMonoidal CartesianMonoidal \longrightarrow SymmetricMonoidal

    would be the suspension functor Σ \Sigma^{\infty} from the base topos to its spectrum objects. (?)

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeDec 9th 2013

    I haven’t written down anything about this yet. But #21 is exactly right. When you generalize from a nonlinear/linear monoidal adjunction to an indexed monoidal category, which corresponds to introducing dependency of linear types on nonlinear ones, the “linearization” operator becomes the functor Σ=π !π *\Sigma = \pi_! \pi^* from the base category to the fiber over *\ast discussed on p595 of Duality and traces for indexed monoidal categories.

    If we denote two-sorted contexts by Γ|Θ\Gamma | \Theta, where Γ\Gamma is nonlinear and Θ\Theta is linear, then given a nonlinear type

    |A:Type \cdot | \cdot \vdash A : Type

    we have the unit linear type

    |I:LType \cdot | \cdot \vdash I : LType

    which we can base change to AA:

    (x:A)|I:LType (x:A) | \cdot \vdash I : LType

    and then take a dependent sum (the dependent sum of a family of linear types over a nonlinear type is one of the basic operations, which corresponds categorically to pushforward):

    |( (x:A)I):LType. \cdot | \cdot \vdash \Big(\sum_{(x:A)} I\Big) : LType.
    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013
    • (edited Dec 10th 2013)

    Ah, now i understand: it exists, but only inside you at the moment. That’s good to know.

    That construction you describe applied more generally to dependent linear homotopy types will be the generalized Thom spectrum construction (as here), I suppose.

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeDec 10th 2013

    Yes, exactly.

    I think the closest type-theoretic literature I’ve found to what I’m thinking of is this. There could very well be more out there that I haven’t found, though.

    • CommentRowNumber25.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 10th 2013

    If, as I mentioned above, dependent sum type has:

    One might expect that in “dependent linear type theory” the positive and negative dependent sums would become different. However, the meaning of the quoted phrase is unclear,

    and, as Mike says,

    the dependent sum of a family of linear types over a nonlinear type is one of the basic operations, which corresponds categorically to pushforward,

    then are we seeing again a difference of two pushforwards of the kind Urs mentioned here?:

    Generally, six-operations Yoga is at its heart about characterizing how in the presence of two different pullbacks f !f^!, f *f^\ast or in the presence of two different push-forwards f *f_\ast, f !f_!, one may differ from the other only by a composite of dualizing and tensoring with a correction factor

    • CommentRowNumber26.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 10th 2013

    Is there a general theme about when linearizing, two things become separate and we’re interested in the difference? E.g., the Goodwillie claims I’ve mentioned before:

    There are in some sense exactly two tangent connections on the category of spaces (or should we say on any model category?). Both are flat and torsion-free. There is a map between them, so it is meaningful to subtract them.

    and

    their difference is the tensor field known as smash product of spectra.

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013

    @Mike, thanks, I have added that to the references here.

    @David, I am not the one to say anything about the negative/positive issue, but the two different push-forwards f !f_! and f *f_\ast correspond to the two different quantifiers: dependent sum and dependent product.

    Concerning the last question: it would surprise me if that statement of Goodwillie were an example of a general theme instead of a peculiar property of spectra. But then, that whole statement is still pretty mysterious to me, so I might be entirely wrong.

    • CommentRowNumber28.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 10th 2013

    Hmm, don’t we need the positive/negative polarity aspect to get at the full range of linear logic connectives? Multiplicative conjunction and additive disjunction are both positive types, while the additive conjunction and multiplicative disjunction are negative types. Wouldn’t we expect then two kinds of dependent sum as a kind of generalised product? Could it be that all the six operations without identification are needed?

    About Goodwillie, for what it’s worth, the full abstract is

    Title: Geometric Language for the Functor/Function Analogy

    Abstract: This talk is about a point of view. Functors TOP—SPECTRA that preserve weak homotopy equivalences may be considered as global functions on the variety TOP. We sketch a dictionary for this kind of geometry. Functors TOP/B—SPECTRA on the category of spaces over a fixed space B serve as functions in a neighborhood of the point B. The tangent space of TOP at B is the category of parametrized spectra over B. There are cotangent vectors, tensor fields both covariant and contravariant, and differential operators.

    There are precisely two tangent connections, both flat, and their difference is the tensor field known as smash product of spectra. I cannot find differential forms (except 0-forms and 1-forms). This has not yet led to nontrivial theorems, but I will at least say something trivial about some nontrivial examples.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeDec 10th 2013

    The dependent sum that I mentioned is definitely a positive type, and Urs is right that the “other pushforward” is a dependent product rather than a dependent sum. It’s an interesting question whether there is a negative linear dependent sum type! I don’t see what it would mean semantically in terms of indexed monoidal categories, or how to define it in this sort of dependent linear type theory. Note that the positive dependent sum I described above is only “half linear”: it is the sum of a family of linear types indexed over a nonlinear type, and it is itself a linear type. The “first projection”, which seems essential to make sense of a negative dependent sum, would therefore have to be a term inhabiting a nonlinear type in a nonempty linear context, and the type theory I have in mind doesn’t allow such things — because I don’t know what they would mean semantically. Maybe if we knew what it meant for a linear type to depend on another linear type, then we could make sense of both polarities of dependent sum.

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeDec 10th 2013

    And if anyone figures out what Goodwillie is talking about, I’d love to hear it. (-:

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013
    • (edited Dec 10th 2013)

    a term inhabiting a nonlinear type in a nonempty linear context, and the type theory I have in mind doesn’t allow such things — because I don’t know what they would mean semantically.

    Consider a tangent \infty-topos. Its types are already in themselves linear types dependent on non-linear types in some way. Now go to the slices of that and find a semantics that has linear and non-linear types depend on linear and non-linear types.

    At least this is so after one declares a monoidal product on the linear types depending on the non-linear types. But we know it exists, it’s the relative smash product of spectrum objects.

    (I am wondering if maybe we can build for each E E_\infty-ring EE an EE-tangent \infty-topos whose objects are parameterized EE-modules…)

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeDec 10th 2013
    • (edited Dec 10th 2013)

    In the internal logic of a tangent \infty-topos, all types are nonlinear. It’s only when you “decompose” that \infty-topos into an indexed monoidal category over the base \infty-topos that you see a bifurcation into linear and nonlinear.

    Maybe you are thinking of iterating the tangent construction? I think then we would have three-sort contexts Γ|Θ|Δ\Gamma | \Theta | \Delta in which Γ\Gamma is nonlinear and both Θ\Theta and Δ\Delta are linear, and each context can depend on the context to the left, so you would have the linear types in Δ\Delta depending on the linear types in Θ\Theta. That might be interesting to think about. But you still wouldn’t have linear types depending on linear types of the same sort, or nonlinear types depending on linear types, so I don’t yet see a “linear-over-linear” dependent sum that would have a meaningful first projection.

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013
    • (edited Dec 10th 2013)

    Hm, while there is more dependence than a naive axiomatization might presuppose, it does decompose and the internal logic sees this: those homotopy types which are stable homotopy types are the linear ones. So the internal logic knows about stable homotopy types depending on stable homotopy types. Just that in general the dependence can also be more intrincate.

    Of course you may want a specific axiomatization that does not allow this. I just thought since you were wondering about semantics this might be worth looking into. We already know that tangent homotopy type theory is relevant/has a good raison d’être and we see that it combines linear and non-linear dependent types, so it might be worth turning the question around and asking which syntaxt captures this kind of tangent semantics.

    It would seem to me also to be desireable to embed linear type theory this way into ordinary type theory instead of making it branch off by itself, for it would mean that all the power of ordinary type theory can be used to analyze the linear type theory inside it.

    No?

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013

    I have added to dependent linear type theory in a new section Properties – The canonical co-modality a remark on what you (Mike) said above in #22, now that I see it in Ponto-Shulman12.

    (But maybe we should rather discuss this further in the thread on dependent linear type theory…)

    • CommentRowNumber35.
    • CommentAuthorMike Shulman
    • CommentTimeDec 11th 2013

    The linear type theory doesn’t sit inside the nonlinear type theory of the tangent category, not in a fully dependent way. For instance, the tensor product is not (as far as I know) a type-theoretic operation on the nonlinear type theory of the tangent category, because it doesn’t act in all contexts. If (x:X)(A(x):Type)(x:X)\vdash (A(x):Type) and (x:X)(B(x):Type)(x:X)\vdash (B(x):Type) are two dependent types therein, can you define (x:X)(A(x)B(x):Type)(x:X)\vdash (A(x)\otimes B(x):Type)?

    • CommentRowNumber36.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 11th 2013
    • (edited Dec 11th 2013)

    Re #29, does this mean that linear dependent sum and linear dependent product are intertwined by weak duality?

    Oh I see. It’s something like

    x:A[B,I][ x:AB,I]. \product_{x:A}[B, I] \cong [\sum_{x:A} B, I].
    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeDec 11th 2013

    @David: Yes. More generally, if (x:A)(B(x):LType)(x:A)\vdash (B(x):LType) is a dependent linear type (with AA nonlinear) and (C:LType)\cdot \vdash (C:LType) is any non-dependent linear type, then we have

    ( x:A(B(x)C))=( x:AB(x))C. \Big(\prod_{x:A} (B(x)\multimap C)\Big) = \Big(\sum_{x:A} B(x) \Big) \multimap C.
    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeJan 12th 2014
    • (edited Jan 12th 2014)

    Just a comment to myself, for completeness:

    there is some kind of relation of the above also to relative monads and their Kleisli categories. It is now slowly dawning on me that Thorsten Altenkirch’s discussion of quantum computation in terms of (relative) monads is not so unrelated to the pull-push that I am looking at in “Type-semantics for quantization”. But I need to think more about it.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeFeb 6th 2014
    • (edited Feb 6th 2014)

    Just for the record:

    with an insight from Joost Nuiten we finally found a neat way to at least organize the data of “consistent orientations in pull-push quantization” that made me start this thread here. There is a description now in section 7.3 of my notes.

    It’s encoded as a lax natural transformation out of what is essentially that pull-push “monad-oid”/”polyad” that I was wondering about above (only that in the present form of the notes I don’t actually consider the monadic products yet). Hence I suppose this is, or would be, indeed an element of the “collage” of that, as Mike pointed out above in #5.