Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 complex complex-geometry computable-mathematics computer-science constructive cosmology definitions 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

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 17th 2025
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexA prominent choice when illustrating the notion of [[double category]] is that of $\mathbb{R}ing$, the double category of rings, ring morphisms, bimodules and bimodule morphisms. I wonder if there's any connection to the fact that the [[tangent category]] to the category of (not necessarily commutative) rings at $R$ is the category of $R$-bimodules. It's as though the tangent category has picked up on paths in the infinitesimal neighborhoods of the points. You could imagine the double category as expanding the tangent category to paths beyond the infinitesimal. Anything to this thought? It would be something like using the two directions of a double category to deal with the nonlinear and linear aspects. Of course we have the interesting phenomenon of the tangent to $\infty-Grpd$ still being a topos. Might this profit though from 'expanding' the linear dimension? I wonder if there's something misleading in that when the nonlinear objects are commutative, one doesn't speak of bimodules. So the tangent category to $CRing$ is just $Mod$. But could one think of this as morally, $T_R(Ring) = R-R-BiMod$. What would be the opening up of the linear dimension in the case of parameterized spectra? Something like $ X \times Y^{op} \to Spec$? Maybe there's something misleading with $Y^{op} \cong Y$. Hmm, just had a sense that I should take a look at [Entanglement of Sections](https://ncatlab.org/schreiber/show/Entanglement+of+Sections).

   A prominent choice when illustrating the notion of double category is that of $\mathbb{R}ing$, the double category of rings, ring morphisms, bimodules and bimodule morphisms. I wonder if there’s any connection to the fact that the tangent category to the category of (not necessarily commutative) rings at $R$ is the category of $R$-bimodules.

   It’s as though the tangent category has picked up on paths in the infinitesimal neighborhoods of the points. You could imagine the double category as expanding the tangent category to paths beyond the infinitesimal. Anything to this thought?

   It would be something like using the two directions of a double category to deal with the nonlinear and linear aspects. Of course we have the interesting phenomenon of the tangent to $\infty-Grpd$ still being a topos. Might this profit though from ’expanding’ the linear dimension?

   I wonder if there’s something misleading in that when the nonlinear objects are commutative, one doesn’t speak of bimodules. So the tangent category to $CRing$ is just $Mod$. But could one think of this as morally, $T_R(Ring) = R-R-BiMod$.

   What would be the opening up of the linear dimension in the case of parameterized spectra? Something like $X \times Y^{op} \to Spec$? Maybe there’s something misleading with $Y^{op} \cong Y$.

   Hmm, just had a sense that I should take a look at Entanglement of Sections.

2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 17th 2025
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI knew something felt familiar. [Here's](https://golem.ph.utexas.edu/category/2006/11/klein_2geometry_vii.html#c005987) a discussion from ages ago about why we tend not to bother to say 'birepresentation' when it comes to groups, because a $G-H$-birepresentation is a $G \times H$-representation.

   I knew something felt familiar. Here’s a discussion from ages ago about why we tend not to bother to say ’birepresentation’ when it comes to groups, because a $G-H$-birepresentation is a $G \times H$-representation.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 17th 2025
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexAh, this from [[external tensor product]] seems relevant: > Under suitable conditions on compact generation of $Mod(-)$ then one may deduce that $Mod(X_1 \times X_2)$ is generated under external product from $Mod(X_1)$ and $Mod(X_2)$,

   Ah, this from external tensor product seems relevant:

   Under suitable conditions on compact generation of $Mod(-)$ then one may deduce that $Mod(X_1 \times X_2)$ is generated under external product from $Mod(X_1)$ and $Mod(X_2)$,

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeFeb 17th 2025
   • (edited Feb 17th 2025)
   • PermaLink
   Author: Urs
   Format: MarkdownItexJust to highlight, as you note, that those bimodules appearing as Beck modules ([here](https://ncatlab.org/nlab/show/Beck+module#OverAssociativeAlgebras)) have the same ring acting on both sides (in the commutative case these actions can and do coincide), while the bimodules in that double category may generally have different rings acting on either side. Another issue to beware for your question is that the tangent/Beck module construction does not know about the composition of bimodules (as far as I am aware), whereas this is, of course, a key part of the double category structure.

   Just to highlight, as you note, that those bimodules appearing as Beck modules (here) have the same ring acting on both sides (in the commutative case these actions can and do coincide), while the bimodules in that double category may generally have different rings acting on either side.

   Another issue to beware for your question is that the tangent/Beck module construction does not know about the composition of bimodules (as far as I am aware), whereas this is, of course, a key part of the double category structure.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeFeb 17th 2025
   • PermaLink
   Author: Urs
   Format: MarkdownItexOn the "birepresentations": Strictly speaking, $(G,H)$-birepresentations are $G \times H^{op}$-representations, for $H^{op}$ the "opposite group", just as $(A,B)$-bimodules are $A \otimes B^{op}$-modules. So the real point here is that groups $H$ are always canonically isomorphic to their opposite groups (via the inversion map) and that the analogue of this statement fails for rings. That's why why one speaks of bimodules but not so much about "birepresentations".

   On the “birepresentations”: Strictly speaking, $(G,H)$-birepresentations are $G \times H^{op}$-representations, for $H^{op}$ the “opposite group”,

   just as $(A,B)$-bimodules are $A \otimes B^{op}$-modules.

   So the real point here is that groups $H$ are always canonically isomorphic to their opposite groups (via the inversion map) and that the analogue of this statement fails for rings. That’s why why one speaks of bimodules but not so much about “birepresentations”.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 17th 2025
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThanks. > Another issue to beware for your question is that the tangent/Beck module construction does not know about the composition of bimodules (as far as I am aware), whereas this is, of course, a key part of the double category structure. Wouldn't this be a good thing to have, though? So the tangent construction is picking up say a parameterized spectrum at an $\infty$-groupoid $X$, and while we may composed two of these with the external tensor product to a spectrum parameterized over $X \times X$, were to see one of these parameterized spectra as some kind of $X$-$X^{op}$-bimodule, then two of them should compose to give just another $X$-parameterized spectrum. Is that the issue?

   Thanks.

   Another issue to beware for your question is that the tangent/Beck module construction does not know about the composition of bimodules (as far as I am aware), whereas this is, of course, a key part of the double category structure.

   Wouldn’t this be a good thing to have, though? So the tangent construction is picking up say a parameterized spectrum at an $\infty$-groupoid $X$, and while we may composed two of these with the external tensor product to a spectrum parameterized over $X \times X$, were to see one of these parameterized spectra as some kind of $X$-$X^{op}$-bimodule, then two of them should compose to give just another $X$-parameterized spectrum. Is that the issue?

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 17th 2025
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexBut there is a parameterized smash product, so no.

   But there is a parameterized smash product, so no.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeFeb 17th 2025
   • PermaLink
   Author: Urs
   Format: MarkdownItexIncidentally, a parameterized spectrum on a connected space $X$ is an $\infty$-representation of the loop $\infty$-group $\Omega X$ (because $X \simeq B \Omega X$), and the above comments about bi-representations apply here, too, in homotopified form. In this context, we are looking at $G$-representations [[infinity-representation|as]] linear fibrations over $B G$. Given two such, you want to tensor them to a fibration over the point. This will be given by a homotopy coend formula, as usual for tensor products.

   Incidentally, a parameterized spectrum on a connected space $X$ is an $\infty$-representation of the loop $\infty$-group $\Omega X$ (because $X \simeq B \Omega X$), and the above comments about bi-representations apply here, too, in homotopified form.

   In this context, we are looking at $G$-representations as linear fibrations over $B G$. Given two such, you want to tensor them to a fibration over the point. This will be given by a homotopy coend formula, as usual for tensor products.

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 17th 2025
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexPresumably there is then the usual coend calculus to compose parameterization by $X \times Y^{op}$ with that by $Y \times Z^{op}$. By the way, the original motivation for all this was a thought that bunched logic might be better served double category-theoretically. Syntactical complexity is often found to be a sign that one is trying to do two things that should be separate in the same system. They're devising relevant type theories now, such as [here](https://arxiv.org/abs/2501.17869).

   Presumably there is then the usual coend calculus to compose parameterization by $X \times Y^{op}$ with that by $Y \times Z^{op}$.

   By the way, the original motivation for all this was a thought that bunched logic might be better served double category-theoretically. Syntactical complexity is often found to be a sign that one is trying to do two things that should be separate in the same system. They’re devising relevant type theories now, such as here.

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeFeb 17th 2025
    • PermaLink
    Author: Urs
    Format: MarkdownItexOne day somebody will pick up that bunched homotopy type theory again. Fingers crossed. Meanwhile, I console myself by knowing it's the type-theoretic analog of EPR phenomena ([Monadology, p. 18](https://ncatlab.org/schreiber/files/QuantumMonadology-250206.pdf#page=18)) and as such deservedly hard to grasp.

    One day somebody will pick up that bunched homotopy type theory again. Fingers crossed.

    Meanwhile, I console myself by knowing it’s the type-theoretic analog of EPR phenomena (Monadology, p. 18) and as such deservedly hard to grasp.

11. • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 17th 2025
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexWell, I'm speaking to Oxford computer scientists about such matters on Friday. Odd though. The departmental closure sees me move to this current AI project. I start working on graded monads, cost analysis and amortization, and before I know it we've got copresheaves over an ordered monoid, and it's how do we deal with the linear/nonlinear issue. And then people are telling us to look at bunched logic. No escape! Maybe it's not so surprising. The amortization idea, which is to level out payments of whatever -- time/space/money/memory/computing resource -- over the life of the run of a program, often talk about the Physicist's method, which is to keep track of a 'potential', so that you're stacking up credit in the cheaper times for when the big cost comes.

    Well, I’m speaking to Oxford computer scientists about such matters on Friday.

    Odd though. The departmental closure sees me move to this current AI project. I start working on graded monads, cost analysis and amortization, and before I know it we’ve got copresheaves over an ordered monoid, and it’s how do we deal with the linear/nonlinear issue. And then people are telling us to look at bunched logic. No escape!

    Maybe it’s not so surprising. The amortization idea, which is to level out payments of whatever – time/space/money/memory/computing resource – over the life of the run of a program, often talk about the Physicist’s method, which is to keep track of a ’potential’, so that you’re stacking up credit in the cheaper times for when the big cost comes.

12. • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 17th 2025
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexBy the way, it feels like we need yet another dimension. Not only relating spectra over parameter spaces via bimods, but relating different versions of linearity, $E_{\infty$-rings. Is there ever a need to pass between $R$-linear and $S$-linear tangent $\infty$-toposes? A triple category of spaces and maps, bimodules of parameterized $R$-modules, and $R-S$-bimodules.

    By the way, it feels like we need yet another dimension. Not only relating spectra over parameter spaces via bimods, but relating different versions of linearity, -rings. Is there ever a need to pass between $R$-linear and $S$-linear tangent $\infty$-toposes?

    A triple category of spaces and maps, bimodules of parameterized $R$-modules, and $R-S$-bimodules.

13. • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 17th 2025
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThat's interesting. In Mike Shulman's [Framed bicategories and monoidal fibrations](https://arxiv.org/abs/0706.1286), he writes > There is a double category of parametrized spectra called Ex, whose construction is essentially contained in [MS06]... In [MS06] this structure is described only as a bicategory with ‘base change operations’, but it is pointed out there that existing categorical structures do not suffice to describe it. We will see in §14 how this sort of structure gives rise, quite generally, not only to a double category, but to a framed bicategory, which supplies the missing categorical structure. And > The theory of framed bicategories was largely motivated by the desire to find a good categorical structure for the theory of parametrized spectra in [MS06]. The reader familiar with [MS06] should find the idea of a framed bicategory natural; it was realized clearly in [MS06] that existing categorical structures were inadequate to describe the combination of a bicategory with base change operations which arose naturally in that context. [MS06] is * J. P. May and J. Sigurdsson. [Parametrized Homotopy Theory](https://arxiv.org/abs/math/0411656), volume 132 of Mathematical Surveys and Monographs. Amer. Math. Soc., 2006.

    That’s interesting. In Mike Shulman’s Framed bicategories and monoidal fibrations, he writes

    There is a double category of parametrized spectra called Ex, whose construction is essentially contained in [MS06]… In [MS06] this structure is described only as a bicategory with ‘base change operations’, but it is pointed out there that existing categorical structures do not suffice to describe it. We will see in §14 how this sort of structure gives rise, quite generally, not only to a double category, but to a framed bicategory, which supplies the missing categorical structure.

    And

    The theory of framed bicategories was largely motivated by the desire to find a good categorical structure for the theory of parametrized spectra in [MS06]. The reader familiar with [MS06] should find the idea of a framed bicategory natural; it was realized clearly in [MS06] that existing categorical structures were inadequate to describe the combination of a bicategory with base change operations which arose naturally in that context.

    [MS06] is

    • J. P. May and J. Sigurdsson. Parametrized Homotopy Theory, volume 132 of Mathematical Surveys and Monographs. Amer. Math. Soc., 2006.
14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeFeb 18th 2025
    • PermaLink
    Author: Urs
    Format: MarkdownItexIt sounds a bit like "double category" is the answer you want, and now you are looking for the question. ;-) Just to note that in the situation of $R$-linear fibrations over $B G$, base change corresponds to forming induced/restricted/co-induced reps (as recorded in our [[homotopy type representation theory -- table]]).

    It sounds a bit like “double category” is the answer you want, and now you are looking for the question. ;-)

    Just to note that in the situation of $R$-linear fibrations over $B G$, base change corresponds to forming induced/restricted/co-induced reps (as recorded in our homotopy type representation theory – table).

15. • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 18th 2025
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexSo re #8, isn't the situation a little like: > The double category of sets, functions and relations is all well and good, but we can always reconstruct everything from self-relations on sets (a relation between $A$ and $B$ is a self-relation on $A \coprod B$). And then even further it's all just about properties, a relation between $A$ and $B$ is just a property of $A \times B$. So really all we need are sets, functions and properties/subsets. But advantages are gained by working with double categories.

    So re #8, isn’t the situation a little like:

    The double category of sets, functions and relations is all well and good, but we can always reconstruct everything from self-relations on sets (a relation between $A$ and $B$ is a self-relation on $A \coprod B$). And then even further it’s all just about properties, a relation between $A$ and $B$ is just a property of $A \times B$. So really all we need are sets, functions and properties/subsets.

    But advantages are gained by working with double categories.

16. • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeFeb 18th 2025
    • PermaLink
    Author: Urs
    Format: MarkdownItex> advantages are gained by working with double categories. A major one being that one can write more articles on formalism. ;-) Seriously, you may first want to have a clearer picture of what you are trying to prove or to model, and when that picture is clear it's time to look for tools.

    advantages are gained by working with double categories.

    A major one being that one can write more articles on formalism. ;-)

    Seriously, you may first want to have a clearer picture of what you are trying to prove or to model, and when that picture is clear it’s time to look for tools.

17. • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 18th 2025
    • (edited Feb 18th 2025)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexOur comment crossed by the way. #15 wasn't responding to #14. Maybe I'm looking to force things a little. But sometimes that's not such a bad thing. Anyway, double categories are very much in where I'm working now. Edit: must remember to refresh. This wasn't a response to your last one.

    Our comment crossed by the way. #15 wasn’t responding to #14.

    Maybe I’m looking to force things a little. But sometimes that’s not such a bad thing. Anyway, double categories are very much in where I’m working now.

    Edit: must remember to refresh. This wasn’t a response to your last one.

18. • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 19th 2025
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItex> you may first want to have a clearer picture of what you are trying to prove or to model Does LHoTT/QS deal with situations where the choice of worlds (choice of measurement basis) is not predetermined? I take it there's no reason it shouldn't represent the experimental protocol for Aspect-like experiments, where some indeterminacy decides which measurements to take on part of an entangled system. Can the Heisenberg uncertainty principle be represented?

    you may first want to have a clearer picture of what you are trying to prove or to model

    Does LHoTT/QS deal with situations where the choice of worlds (choice of measurement basis) is not predetermined? I take it there’s no reason it shouldn’t represent the experimental protocol for Aspect-like experiments, where some indeterminacy decides which measurements to take on part of an entangled system.

    Can the Heisenberg uncertainty principle be represented?

19. • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeFeb 19th 2025
    • PermaLink
    Author: Urs
    Format: MarkdownItexOn the first question: A key aspect of the setup is that it retains full classical programming logic, so that all operations can be subjected to case distinctions like "if measurement gives such-and-such then next measure this, else measure that". This just corresponds to handling indexed sets of possible worlds and then picking an index value. This possibility of classical control over quantum operations is what the diagram on [p. 4](https://arxiv.org/pdf/2310.15735#page=4) means to highlight. On a side note, it may be, say, entertaining to realize the sheer scale of this classical intervention into quantum computation that the currently dominant idea of future "quantum error correction" of noisy qbits (NISQ+QEC) is envisioning: The left column of p. 5 in Waintal 2024 "The Quantum House of Cards" ([arXiv:2312.17570](https://arxiv.org/abs/2312.17570)) gives some impression. This is why the NISQ+QEC program has been likened to the search for perpetual motion of previous centuries (by [Kalai 2012](https://rjlipton.com/2012/01/30/perpetual-motion-of-the-21st-century/)). But I am seriously digressing now... $\,$ On the second question: The phenomenon of Heisenberg uncertainty directly reflects the non-commutativity of observables in quantum probability. That non-commutativity is reflected in the language: Ex. 2.44 ([p. 87](https://arxiv.org/pdf/2310.15735#page=87)). Note though that this is not to do with dependent types. For instance the [[ZX-calculus]] gets its name from a pair of non-commuting observables: $Z$ and $X$, and draws its interest from the useful consequences of their Heisenberg uncertainty, if you wish.

    On the first question:

    A key aspect of the setup is that it retains full classical programming logic, so that all operations can be subjected to case distinctions like “if measurement gives such-and-such then next measure this, else measure that”. This just corresponds to handling indexed sets of possible worlds and then picking an index value.

    This possibility of classical control over quantum operations is what the diagram on p. 4 means to highlight.

    On a side note, it may be, say, entertaining to realize the sheer scale of this classical intervention into quantum computation that the currently dominant idea of future “quantum error correction” of noisy qbits (NISQ+QEC) is envisioning: The left column of p. 5 in Waintal 2024 “The Quantum House of Cards” (arXiv:2312.17570) gives some impression. This is why the NISQ+QEC program has been likened to the search for perpetual motion of previous centuries (by Kalai 2012). But I am seriously digressing now…

    $\,$

    On the second question:

    The phenomenon of Heisenberg uncertainty directly reflects the non-commutativity of observables in quantum probability. That non-commutativity is reflected in the language: Ex. 2.44 (p. 87). Note though that this is not to do with dependent types. For instance the ZX-calculus gets its name from a pair of non-commuting observables: $Z$ and $X$, and draws its interest from the useful consequences of their Heisenberg uncertainty, if you wish.

20. • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 19th 2025
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexA sobering article by Waintal! Topological protection to the rescue. Re my questions, thanks! Right, so I was fishing for some need to have some structure in the parameterization, so that there might be some genuine $X-Y$-bimodule behaviour. But maybe the way to think is that whatever the situation, whenever there's a measurement, it takes place in the context of one set of outcomes. A change of basis is just that. Product of parameter sets is possible, but there won't be any $W-W'$ and $W'-W''$, therefore $W-W''$. Just to mention, since I guess the coloured palette approach to bunched types isn't written in stone as the only way to do linear HoTT, but there are other attempts to derive a substructural dependent type theory, such as * {#Aberle24b} [[C.B. Aberlé]], *Foundations of Substructural Dependent Type Theory* [[arXiv:2401.15258](https://arxiv.org/abs/2401.15258)]

    A sobering article by Waintal! Topological protection to the rescue.

    Re my questions, thanks! Right, so I was fishing for some need to have some structure in the parameterization, so that there might be some genuine $X-Y$-bimodule behaviour. But maybe the way to think is that whatever the situation, whenever there’s a measurement, it takes place in the context of one set of outcomes. A change of basis is just that. Product of parameter sets is possible, but there won’t be any $W-W'$ and $W'-W''$, therefore $W-W''$.

    Just to mention, since I guess the coloured palette approach to bunched types isn’t written in stone as the only way to do linear HoTT, but there are other attempts to derive a substructural dependent type theory, such as

    • {#Aberle24b} C.B. Aberlé, Foundations of Substructural Dependent Type Theory [arXiv:2401.15258]
21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeFeb 19th 2025
    • (edited Feb 19th 2025)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks for the pointer, have now listed that reference also at *[[dependent linear types]]*. But does it handle [[doubly closed monoidal category|doubly closed monoidal]] structure? After a first scan through the article it seems not to do so, but maybe I missed it.

    Thanks for the pointer, have now listed that reference also at dependent linear types.

    But does it handle doubly closed monoidal structure? After a first scan through the article it seems not to do so, but maybe I missed it.

22. • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 19th 2025
    • (edited Feb 19th 2025)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI never find it easy to extract what type theorists are up to. By the time we get to the end (4.1 Toward the type theory of monoidal topoi) there's talk of how to relate the two monoidal structures on a monoidal topos and the need for two left-fibrant structures on the same double category. And then some speculation that there should be a connection to Mitchell's work.

    I never find it easy to extract what type theorists are up to. By the time we get to the end (4.1 Toward the type theory of monoidal topoi) there’s talk of how to relate the two monoidal structures on a monoidal topos and the need for two left-fibrant structures on the same double category. And then some speculation that there should be a connection to Mitchell’s work.

23. • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 20th 2025
    • (edited Feb 20th 2025)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexFor what it's worth, I see that Peter May in [these slides](https://www.math.uchicago.edu/~may/TALKS/MichiganPrint.pdf) turns to bicategories and bimodules precisely at the moment he treats Costenoble-Waner duality: > the notion of Costenoble–Waner duality, the parametrised (as opposed to fibrewise) version of Spanier-Whitehead duality, ([here](https://arxiv.org/pdf/1705.06232#page=17))

    For what it’s worth, I see that Peter May in these slides turns to bicategories and bimodules precisely at the moment he treats Costenoble-Waner duality:

    the notion of Costenoble–Waner duality, the parametrised (as opposed to fibrewise) version of Spanier-Whitehead duality, (here)