We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.

翻译：我们研究的是经销商引发的羊羔计算法双分类模型,证明它们可以通过交叉类型系统以综合方式展示。我们首先引入了代数为一元类建模资源管理的二元类。我们把这些月经向经销商举起,并定义了准数Kleisli双类,为关闭其木耳机提供了充分的条件。在此框架内,我们定义了一种与证据相关的语义:对一个与其关联的术语的解释,在适当的系统中对其输入的一组衍生数据加以解释。我们证明,我们的模型具有可溶性,根据我们所处的环境调整了可复制技术。我们最后描述了我们建造的两个例子。