Section 2 of this draft by Mike Shulman explains how Cartesian multicategories are able to directly internalize the structural rules of simple intuitionistic type theory as it is usually presented, and thus characterize the categorical product as an object with a "mapping out" universal property (corresponding to the presentation of the product type as a positive type).

In Section 1 of the same draft, the author remarks that ordinary categories would be the counterpart in this setting to the so-called unary type theories, where there is only one term allowed on each side of a sequent. These are strong enough to present coproducts positively and products negatively, i.e. with a "mapping in" universal property. In contrast, Cartesian multicategories are strong enough to present products positively and exponentials negatively.

It feels like a natural next step, then, to look for a category-like structure in which exponential objects can be presented positively. According to this ncatlab article, expressing the function type as a positive type requires a metatheory capable of handling higher-order judgments (where sequents are allowed to appear inside other sequents). If I'm not mistaken, this would correspond categorically to some sort of Cartesian "metacategory" (this is definitely not the correct name), where a "metamorphism" can itself act as a source for other "metamorphisms".

This seems somewhat reminiscent of the notion of 2-category, except that instead of having 1-morphisms between objects and 2-morphisms between 1-morphisms, here we have only one type of "metamorphism", that links a list of "metamorphisms" and objects with a single object. The concept seems simple enough to be well-known, perhaps as a special example of a more general structure like an enriched category, but I haven't been able to find it anywhere so far, most likely due to my lack of knowledge about this topic.

My question is:

Has this structure been named or described somewhere in the literature? Is there any reference where I can learn more about it?

Edit: I did my best to translate the type-theoretic positive presentations mentioned above to commutative diagrams. The dashed arrow indicates unique existence as usual. In the first case it leads to the usual definition of the coproduct as a colimit; the second and third diagrams are clear generalizations.a I think this shows best the analogy between the three structures (please excuse the bad quality, you can click on the image to make it bigger):

Categorical translation of positive type presentations

What I'm looking for is the structure where the "arrows coming out from arrows" in the third diagram make sense.

a: Note that for clarity purposes I omitted some possible extra sources for the multimorphisms and "metamorphisms" in the second and third diagrams. This corresponds type-theoretically to ignoring possible extra contexts $\Gamma$, $\Delta$, etc. in the definitions of the type constructor and eliminator.

  • $\begingroup$ All I can say is that the discussion on nLab makes no sense to me. Can this notion of defining a function type by mapping out be described categorically, instead of type theoretically? This isn't the same as your question, since for instance I can understand Cartesian closed categories as giving a "positive" description of products. $\endgroup$ – Kevin Carlson Oct 29 '18 at 5:32
  • $\begingroup$ @KevinCarlson The terminology Shulman uses is perhaps a bit confusing. By "mapping out" property he refers to a colimit-like presentation, where a unique morphism is defined that maps out of the object. The usual definition of a exponential object in a category would be through a "mapping in" property, since the transpose morphism maps into the object. I added an image that hopefully clarifies my question a little. $\endgroup$ – pregunton Oct 29 '18 at 8:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.