We present an extension of Martin-L\"of Type Theory that contains a tiny object; a type for which there is a right adjoint to the formation of function types as well as the expected left adjoint. We demonstrate the practicality of this type theory by proving various properties related to tininess internally and suggest a few potential applications.

翻译：我们提出马丁-洛夫类型论的一种扩展，其中包含一个极小对象：即该类型不仅具有预期的左伴随，还同时存在对函数类型构成右伴随的伴随。通过内部证明与极小性相关的若干性质，我们论证了该类型论的实用性，并提出了几种潜在应用方向。