Internal language theorems are fundamental in categorical logic, since they express an equivalence between syntax and semantics. One of such theorems was proven by Clairambault and Dybjer, who corrected the result originally by Seely. More specifically, they constructed a biequivalence between the bicategory of locally Cartesian closed categories and the bicategory of democratic categories with families with extensional identity types, $\sum$-types, and $\prod$-types. This theorem expresses that the internal language of locally Cartesian closed is extensional Martin-L\"of type theory with dependent sums and products. In this paper, we study the theorem by Clairambault and Dybjer for univalent categories, and we extend it to various classes of toposes, among which are $\prod$-pretoposes and elementary toposes. The results in this paper have been formalized using the proof assistant Coq and the UniMath library.

翻译：内部语言定理在范畴逻辑中具有基础性地位，因为它们表达了语法与语义之间的等价性。Clairambault 与 Dybjer 证明的定理即为一例，该结果修正了 Seely 最初的结论。具体而言，他们建立了局部笛卡尔闭范畴的双范畴与具有外延恒等类型、$\sum$-类型及$\prod$-类型的民主范畴族（democratic categories with families）的双范畴之间的双等价性。该定理表明，局部笛卡尔闭范畴的内部语言即是具有依赖和与依赖积的外延 Martin-Löf 类型论。本文研究 Clairambault 与 Dybjer 的定理在单值范畴中的情形，并将其推广至多种拓扑斯类别，其中包括$\prod$-预拓扑斯与初等拓扑斯。本文的结果已通过证明辅助工具 Coq 及 UniMath 库完成形式化验证。