We present a survey of the two-dimensional and tensorial structure of the lifting doctrine in constructive domain theory, i.e. in the theory of directed-complete partial orders (dcpos) over an arbitrary elementary topos. We establish the universal property of lifting of dcpos as the Sierpi\'nski cone, from which we deduce (1) that lifting forms a Kock-Z\"oberlein doctrine, (2) that lifting algebras, pointed dcpos, and inductive partial orders form canonically equivalent locally posetal 2-categories, and (3) that the category of lifting algebras is cocomplete, with connected colimits created by the forgetful functor to dcpos. Finally we deduce the symmetric monoidal closure of the Eilenberg-Moore resolution of the lifting 2-monad by means of smash products; these are shown to classify both bilinear maps and strict maps, which we prove to coincide in the constructive setting. We provide several concrete computations of the smash product as dcpo coequalisers and lifting algebra coequalisers, and compare these with the more abstract results of Seal. Although all these results are well-known classically, the existing proofs do not apply in a constructive setting; indeed, the classical analysis of the Eilenberg-Moore category of the lifting monad relies on the fact that all lifting algebras are free, a condition that is not known to hold constructively.

翻译：本文综述了构造域论（即任意基本拓扑上的定向完备偏序集理论）中提升学说的二维与张量结构。我们建立了dcpo提升作为Sierpiński锥的泛性质，由此推导出：(1)提升形成Kock-Zöberlein学说；(2)提升代数、尖点dcpo与归纳偏序集构成范畴等价的位置化2-范畴；(3)提升代数范畴是余完备的，其连通余极限由遗忘函子至dcpo生成。最后通过smash积推导了提升2-单子的Eilenberg-Moore分解的对称幺半闭包性质；证明这些smash积在构造框架下同时分类双线性映射与严格映射，且二者等价。我们给出了smash积作为dcpo余等化子与提升代数余等化子的具体构造，并与Seal的抽象结论进行了比较。尽管这些结果在经典情形中广为人知，但现有证明不适用于构造性框架——经典分析中提升单子的Eilenberg-Moore范畴依赖于"所有提升代数皆自由"这一性质，而该条件在构造框架下尚未得到验证。