Substructural logics can be obtained by dropping different structural rules, most commonly contraction, weakening, exchange. Effects of not having these rules have been studied widely in literature, both in classical and constructive settings. But there are some more "structural" rules that are more essential to the systems, that sometimes people don't even mention them unless they are in some ways different than their traditional counterparts. Namely reflexivity and transitivity. Reflexivity is sometimes presented as the "id" rule while transitivity is presented as the "cut" rule. In the literature of non-constructive non-classical logics, logics lacking these rules are called non-reflexive and non-transitive logic respectively. From what I understand both of these logics can be used for transparency of truth and latter can be used for something called paradox tolerance.
After reading about these extreme substructural logics I became curious about their constructive meanings, and how would they behave in a lambda calculus like system. So it occured to me that composition in category theory somewhat corresponds to cut rule in logic, and categories where composition is partially defined are called paracategories. So non-transitive logics must have a model in these "paracategories" but I couldn't find any papers about this, and generally about paracategories. After a while I read about "semicategories" which can be models for non-reflexive logics. But again no luck.
I mean when I think about what could motivate these rather abstract logics in a constructive environment, only thing that occurs to me is that paradox tolerance can be helpful dealing with inconsitent theories within a (para)consistent system. But I can't see if constructive logics could still work without a cut rule.
Shortly, my question is; Are there any research about constructive interpretations and uses of non-reflexive, non-transitive or generally cut-free logics, type theories, and their models in category theory?
EDIT: Here is a table of various substructural logics because I'm learning about formatting and I love structured information, no pun intended.
| Logic | Category | Rules Dropped | Interpretation |
|---|---|---|---|
| Ordered | Non-Symmetric Monoidal Category | $$\frac{\Gamma,\alpha,\beta,\Delta \; \vdash \; \varphi}{\Gamma,\beta,\alpha,\Delta \; \vdash \; \varphi}exchange$$[0] | Arguments must be used in order |
| Linear | Symmetric Monoidal Category | $$\frac{\Gamma,\alpha,\alpha,\Delta \; \vdash \; \varphi}{\Gamma,\alpha,\Delta \; \vdash \; \varphi}contraction \\ \frac{\Gamma,\Delta \; \vdash \; \varphi}{\Gamma,\alpha,\Delta \; \vdash \; \varphi}weakening$$ | Arguments must be used exactly once |
| Affine | Semicartesian Monoidal Category | $$\frac{\Gamma,\alpha,\alpha,\Delta \; \vdash \; \varphi}{\Gamma,\alpha,\Delta \; \vdash \; \varphi}contraction$$ | Arguments must be used at most once |
| Relevance | Relevance Monoidal Category | $$\frac{\Gamma,\Delta \; \vdash \; \varphi}{\Gamma,\alpha,\Delta \; \vdash \; \varphi}weakening$$ | Arguments must be used at least once |
| Non-Associative | Deductive System [1] | $$? \, associativity$$ | Arguments must be used in the same scope structure ? [2] |
| Non-Reflexive | Semicategory | $$\frac{}{\alpha\; \vdash \; \alpha}id$$ | ? |
| Non-Transitive | Paracategory | $$\frac{\Gamma_1 \; \vdash A, \Delta_1 \quad \Gamma_2, A \; \vdash \Delta_2 } {\Gamma_1,\Gamma_2 \; \vdash \; \Delta_1, \Delta_2}cut$$ | ? |
[0]: Apparently ordered logic often follows linear logic, but from what I have seen there is no reason for such a restriction. It could follow from any other classical/non-classical logic.
[1]: I'm not sure about this one that much, but categories where associativity doesn't hold are called such and there aren't many concrete models of non-associative logics in categories. I'm not sure about the rule.
[2]: Again not that sure because only places I have seen non-associative logics used are often lambek calculi and categorical grammars. Nothing all that deep on non-associative aspect of the proof-theory in more abstract sense. What I tried to say there is: from (A * B) * C, we cannot derive A -> (B * C), because they don't have the same "scope" structure. I'm not sure wheter linearity is required or not for this.