Working with \(\Opn\)-CwRs

A judgment is static-modal if \(\Opn\,A \cong A\).

Static-modal judgments when interpreted in indexed presheaves depend only on the base context.

We make the \(\ms{Ty}\) judgment static-modal.

A judgment is dynamic-modal if \(\Opn\,A \cong \top\).

Nothing that depends only on the base context depends on a dynamic-modal judgment.

We make the \(\ms{El}\,A\) judgment dynamic-modal for small \(A\).