 GL fixed point by truth substitution

Let $U=\square Y(\top )$ and $V=\square Y(U)$. Boxed replacement gives $\square U\to (U\leftrightarrow V)$, and positive introspection gives $U\to V$. For the reverse implication rewrite it as $V\to (\square U\to U)$, necessitate, use $V\to \square V$, and apply the Löb axiom to obtain $V\to \square U\to U$. This explicit one-variable construction needs no reflection axiom.