Does $f \leq f \circ f^\dagger \circ f$ hold in an arbitrary allegory? If $f$ is an arrow of $\mathrm{Rel}$, then $f \leq f \circ f^\dagger \circ f.$ _Proof._ Suppose $xy \in f$. Then $xy \in f, yx \in f^\dagger, xy \in f$. Thus $xy \in f \circ f^\dagger \circ f.$ **Question.** Does this inequality hold in an arbitrary allegory?

Yes, apply the _modularity law_

> $\,uv\,\land w\ \le\ (u\land\, wv^\dagger)v\,$

with $v,w=f:A\to B$ and $u:=1_A$. We get $$f\ =\ 1_Af\land f\ \le\ (1_A\land ff^\dagger)f\ \le\ (ff^\dagger)f\,.$$