A Universe of Sorts

§ Diagonal lemma for monotone functions

Statement: For a monotone function $f: P \times P \to Q$ , we have the equality $f(\sqcup_s s, \sqcup_t t) = f(\sqcup_x (x, x))$
Since $\sqcup_x (x, x) \sqsubseteq \sqcup_{s, t} (s, t)$ , by monotonicity of $f$ , we have that $f(\sqcup_x (x, x)) \sqsubseteq f(\sqcup{s, t} (s, t))$ .
On the other hand, note that for each $(s_\star, t_\star)$ , we have that $(s_\star, t_\star) \leq \sqcup (s_\star \sqcup t_\star, t_star \sqcup t_\star) = (s_\star, s_star) \sqcup (t_\star, t_\star)$ . Thus each element on the RHS is dominated by some element on the LHS.
So we must have equality of LHS and RHS.

We wish to prove that $f^n$ is continuous, given that $f$ and $(\circ)$ is continuous.
Proof by induction. $n = 0$ is immediate. For case $n+1$ :

\begin{aligned} &(\sqcup_f f)^{n+1} \\ &= (\sqcup_f f) \circ (\sqcup_g g)^n \\ &= \sqcup_g ((\sqcup_f f) \circ g^n) \\ &= \sqcup_g \sqcup_f (f \circ g^n) \\ &= \sqcup_f (f \circ f^n) \\ &= \sqcup_f (f^{n+1}) \\ \end{aligned}

See that we used the diagonal lemma to convert the union over $f, g$ into a union over $f$ .