\begin{code} module Issue97b where Foo : Set₁ Foo = \end{code} A comment. \begin{code} Set \end{code}