Synthetic topos theory
[001V] Rule

\(\mathord {\textnormal {\textsf {Level}}}\) is a judgment form.