一句话：给出一组弱公理，刻画可在任意拓扑斯内构造基于路径的立方类型理论模型所需条件，并澄清均匀 Kan 填充。
本文研究内涵类型理论的同伦式解释，即把等式证明视为路径。作者追问：在一个拓扑斯中，对象 I 需要满足哪些条件，才能给出以 I 为定义域的函数作为路径的类型论模型。Cohen、Coquand、Huber 与 Mörtberg 曾利用特定预层范畴构造此类模型；本文则考察这一构造在任意拓扑斯的内部类型论中可表达到何种程度，并为此识别出一组相当弱的公理。该公理化刻画澄清了均匀 Kan 填充的定义与性质，而均匀 Kan 填充正是他们构造性解释 Voevodsky 单值公理的核心。本文是发表于 CSL 2016 的同名论文的修订扩充版。
The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object $I$ in a topos to give such a path-based model of type theory in which paths are just functions with domain $I$. Cohen, Coquand, Huber and M\"ortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)