Positive introspection ($\square A\to \square \square A$)

Positive introspection says that a boxed assertion can itself be boxed. For an arithmetical provability predicate it is the third of the Hilbert-Bernays-Löb derivability conditions: provability of $A$ implies provability of the assertion that $A$ is provable. It follows from formalized Sigma-1 completeness when provability assertions are Sigma-1. It is not the reflection principle $\square A\to A$.