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):
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.