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!"