English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present a survey of the two-dimensional and tensorial structure of thelifting doctrine in constructive domain theory. We establish the universalproperty of lifting of directed-complete partial orders (dcpos) as theSierpi\'nski cone, from which we deduce (1) that lifting forms aKock-Z\"oberlein doctrine, (2) that lifting algebras, pointed dcpos, andinductive partial orders form canonically equivalent locally posetal2-categories, and (3) that the category of lifting algebras is cocomplete, withconnected colimits created by the forgetful functor to dcpos. Finally we deducethe symmetric monoidal closure of the Eilenberg-Moore resolution of the lifting2-monad by means of smash products; these are shown to classify both bilinearmaps and strict maps, which we prove to coincide in the constructive setting.We provide several concrete computations of the smash product as dcpocoequalisers and lifting algebra coequalisers, and compare these with the moreabstract results of Seal. Although all these results are well-knownclassically, the existing proofs do not apply in a constructive setting;indeed, the classical analysis of the Eilenberg-Moore category of the liftingmonad relies on the fact that all lifting algebras are free, a condition thatis not known to hold constructively.

Tensorial structure of the lifting doctrine in constructive domain theory