The wikipedia page on the Lambda cube has the following inference rule:
$\frac{\Gamma \vdash A:B \quad B=_\beta B' \quad \Gamma \vdash B':s}{\Gamma \vdash A:B'} \quad \rm (Conversion)$
Why is the assumption $\Gamma \vdash B':s$ necessary? Is it possible to derive a judgement $\Gamma \vdash A:B$ where $B$ is not a type or kind? If not, is it possible for $B$ to be a type or kind and for $B=_\beta B'$ but $B'$ not to be the same type or kind?
Generally speaking, a desirable property of type theory is that a judgement like $\Gamma \vdash t : A$ can only hold if the presupposition that $A$ is a valid type in context $\Gamma$ holds, which in turns presupposes that $\Gamma$ is a well-formed context. This can be proved by structural induction on the inference rules; in order to handle the case for your conversion rule, we need to check that $\Gamma \vdash B' : s$. While we could prove another meta-theorem that says that if $B =_\beta B'$ and $\Gamma \vdash B : s$ then $\Gamma \vdash B' : s$ (subject reduction/expansion), the authors have made the more convenient choice to include the presupposition as an explicit hypothesis.
These things are discussed in the lecture notes Principles of dependent type theory by Carlo Angiuli and Daniel Gratzer, in sections 2.1.3 and 2.2 (look for "presuppositions").
