nLab Phoa's principle

Idea

Let $L$ be a distributive lattice. Phoa’s principle states that for all endofunctions $f:L\to L$ and elements $x \in L$:

$$f(x) = f(\top) \wedge (x \vee f(\bot))$$

In Pos the category of posets and monotonic functions, Phoa’s principle holds for the boolean domain $\mathbb{2}$. In synthetic Stone duality, Phoa’s principle holds for the type of open propositions $\mathrm{Open}$.

Related concepts

• distributive lattice

• flat distributive lattice

• directed univalence

References

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)

• Thierry Coquand, Freek Geerligs, Hugo Moeneclaey, Directed Univalence in Synthetic Stone Duality, unfinished draft; LaTeX documents can be found here.