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.
Added some more intuition for duploids now that I understand them and cbpv better. Duploids only axiomatize effectful morphisms, whereas an adjunction (CBPV) axiomatizes pure morphisms (as homomorphisms) and effectful morphisms (as heteromorphisms). Then thunkable and linear are the maximal way to recover pure morphisms from effectful morphisms. I.e., we should think of duploids as presenting a kind of “Morita equivalence” of adjunctions where we only care about the equivalence of the notion of heteromorphism.
Nice, thanks. Can you give a succinct self-contained definition of a duploid as “an adjunction such that <blank>”? The section “adjunction from a duploid” says that duploids “can be identified with exactly those adjunctions in which all thunkable heteromorphisms are the image under of some homomorphism and vice-versa all linear heteromorphisms are in the image of ” but it’s not obvious to me how to define “thunkable” and “linear” for an adjunction.
What are the morphisms between duploids? Are they the objects of a category? A 2-category? Some fancier structure with more than one kind of morphism, like a double category or an F-category?
In particular, since a duploid can be identified with a particular kind of profunctor, we get two different kinds of morphism between duploids by regarding them as objects of the -autonomous double category (discussed in this blog post and this preprint). Are either of these interesting to duploid theorists?
I’ll write more eventually, but in the mean-time, morphisms of duploids give the morphisms of profunctors that you get from the double category of categories, functors, profunctors and transformations: i.e. A morphism from to has functors from to and to . This should be the right notion of morphism if we’re thinking of an adjunction as a kind of multicategory with 2 modes because it’s a translation of types and morphisms that respects the modes. Is that one of the kinds of morphism in ? I couldn’t find it on that page or the paper (though I was not thorough).
Also I would like to know if the equalising requirement is well known in category theory, because it goes back to Moggi I think in PL theory.
Thanks! Yes, those are one of the kinds of morphisms in , the ones that in the paper I called “vertical”. Perhaps their most explicit description is in the third bullet point below Definition 6.3. The horizontal morphisms are more like “adjunctions” than “functors”; check out for instance examples 6.10 – 6.12.
As for the equalizing requirement, well, it’s true for any monadic adjunction that is the coequalizer of and , and this is one of the inputs of the monadicity theorem. But presumably it’s weaker than monadicity; I don’t recall seeing it exactly before.
1 to 6 of 6