An extension of MLTT that makes an arbitrary ordinary type ๐ tiny, by giving (๐ย โย -) a right adjoint โ. This โ is necessarily not a fibred right adjoint, but is made adjoint to a Fitch-style context lock that represents (๐ย โย -). There is no calculus of explicit substitutions needed, and conjecturally the theory is still normalising.
A 'global sections' modality โญ is not necessary to state the defining adjunction internally, we instead have the more general โ((๐โA)โB) โ (AโโB).
"A root you can compute!"