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