In recent years, Homotopy Type Theory (HoTT) has had great success both as a foundation of mathematics and as internal language to reason about $\infty$-groupoids (a.k.a. spaces). However, in many areas of mathematics and computer science, it is often the case that it is categories, not groupoids, which are the more important structures to consider. For this reason, multiple directed type theories have been proposed, i.e., theories whose semantics are based on categories. In this paper, we present a new such type theory, Twisted Type Theory (TTT). It features a novel ``twisting'' operation on types: given a type that depends both contravariantly and covariantly on some variables, its twist is a new type that depends only covariantly on the same variables. To provide the semantics of this operation, we introduce the notion of dependent 2-sided fibrations (D2SFibs), which generalize Street's notion of 2-sided fibrations. We develop the basic theory of D2SFibs, as well as characterize them through a straightening-unstraightening theorem. With these results in hand, we introduce a new elimination rule for Hom-types. We argue that our syntax and semantics satisfy key features that allow reasoning in a HoTT-like style, which allows us to mimic the proof techniques of that setting. We end the paper by exemplifying this, and use TTT to reason about categories, giving a syntactic proof of Yoneda's lemma.

翻译：近年来，同伦类型论（HoTT）作为数学基础以及作为推理$\infty$-群胚（亦称空间）的内部语言都取得了巨大成功。然而，在数学和计算机科学的许多领域中，通常范畴（而非群胚）才是需要考虑的更重要的结构。因此，学界已提出了多种有向类型论，即其语义基于范畴的类型理论。本文提出了一种新的此类类型论——扭曲类型论（TTT）。其核心特点是引入了一种新颖的类型“扭曲”操作：给定一个在某些变量上既逆变又协变依赖的类型，其扭曲将产生一个仅在这些变量上协变依赖的新类型。为了为此操作提供语义，我们引入了依赖双侧纤维化（D2SFibs）的概念，该概念推广了Street的双侧纤维化概念。我们发展了D2SFibs的基本理论，并通过拉直-非拉直定理对其进行了刻画。基于这些结果，我们为Hom-类型引入了一条新的消去规则。我们论证了我们的语法和语义满足关键特性，使得能够以类似HoTT的风格进行推理，从而可以模仿该框架下的证明技术。最后，我们通过实例说明这一点，并利用TTT对范畴进行推理，给出了米田引理的一个句法证明。