Let Ω be the subobject classifier, or object of truth values, aka propositions or subsingletons. The following discussion works in the internal language of a 1-topos, in HoTT/UF (an internal language for ∞-toposes), and in CZF/IZF (taking Ω = 𝓟 {∅}, the power class/set of the "canonical" singleton set), and possibly more "foundations" or "mathematical worlds". If our (∞-)topos under consideration is boolean, that is, if excluded middle holds in its internal language, there are precisely two automorphisms of Ω, namely the identity map and the negation map. The same is the case for CZF/IZF, and possibly more mathematical worlds. (1) If there is an automorphism f : Ω → Ω such that f(p₀)≠p₀ for some p₀:Ω, then excluded middle holds. Is this fact already known? I recorded my proof somewhere in TypeTopology. Moreover, in order to get the same conclusion, it is enough to assume that f is an embedding, or left-cancellable, meaning that f(p)=f(q) implies p=q. This is because any lc-map Ω → Ω is necessarily an (involutive) automorphism, which is due to Higgs. (2) The converse of (1) also holds trivially, because we can take f to be negation and p₀ to be ⊤ (or ⊥) if excluded middle holds. (1+2) So excluded middle holds if and only if there is an automorphism f : Ω → Ω such that f(p₀)≠p₀ for some p₀:Ω. Any such automorphism f is not the identity map. However, without excluded middle, there is no reason why for any automorphism f≠id there should exist p₀ with f(p₀)≠p₀. So we can't conclude from the above discussion that there is an automorphism different from the identity if and only if excluded middle holds. Can we conclude this by other means? I don't think so, but I don't have a (meta-)proof. 1/

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ński cone, from which we deduce (1) that lifting forms a Kock-Zöberlein 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.