\gdef\jdg#1{\:\mathrm{#1}}
\gdef\decode#1{\mathord{\uparrow}#1}
\gdef\code#1{\mathord{\downarrow}#1}
\gdef\jty{\:\mathrm{ty}}
\gdef\jprop{\:\mathrm{prop}}
\gdef\jtrue{\:\mathrm{true}}
\gdef\yields{\vdash}
\gdef\ms#1{\mathsf{#1}}
\gdef\mc#1{\mathcal{#1}}
\gdef\Open#1{{\Large \circ}{#1}}
\gdef\Close#1{{\Large \bullet}{#1}}
\gdef\OpenEta{\eta^{\circ}}
\gdef\CloseEta{\eta^{\bullet}}
\gdef\isStatic#1{\mathrm{isStatic}(#1)}
\gdef\isDynamic#1{\mathrm{isDynamic}(#1)}
\gdef\ite#1#2#3{\mathbf{if}\:\:#1\:\:\mathbf{then}\:\:#2\:\:\mathbf{else}\:\:#3}
\gdef\StOpn{{\Large \circ}_{\mathrm{st}}}
\gdef\Opn{{\Large \circ}}
\gdef\op{^\mathrm{op}}
\gdef\CC{\mathbb{C}}
Modern approach
-
Introduce a modality \(\StOpn\) to the metatheory
-
Postulate that for types \(A_0,A_1\) we have \(\StOpn(A_0 = A_1) \cong (A_0 = A_1)\)
-
Postulate that for a small type \(A\) we have \(\StOpn(\ms{El}\,A) \cong \top\)
-
Only introduce problematic features at small types