It often happens that free algebras for a given theory satisfy useful reasoning principles that are not preserved under homomorphisms of algebras, and hence need not hold in an arbitrary algebra. For instance, if $M$ is the free monoid on a set $A$, then the scalar multiplication function $A\times M \to M$ is injective. Therefore, when reasoning in the formal theory of monoids under $A$, it is possible to use this injectivity law to make sound deductions even about monoids under $A$ for which scalar multiplication is not injective -- a principle known in algebra as the permanence of identity. Properties of this kind are of fundamental practical importance to the logicians and computer scientists who design and implement computerized proof assistants like Lean and Coq, as they enable the formal reductions of equational problems that make type checking tractable. As type theories have become increasingly more sophisticated, it has become more and more difficult to establish the useful properties of their free models that enable effective implementation. These obstructions have facilitated a fruitful return to foundational work in type theory, which has taken on a more geometrical flavor than ever before. Here we expose a modern way to prove a highly non-trivial injectivity law for free models of Martin-L\"of type theory, paying special attention to the ways that contemporary methods in type theory have been influenced by three important ideas of the Grothendieck school: the relative point of view, the language of universes, and the recollement of generalized spaces.

翻译：对于给定的理论，自由代数通常满足有用的推理原则，但这些原则在代数同态下不一定保持不变，因此未必适用于任意代数。例如，若 $M$ 是集合 $A$ 上的自由幺半群，则标量乘法函数 $A\times M \to M$ 是单射的。因此，在形式化的 $A$ 上幺半群理论中进行推理时，即使对于标量乘法非单射的 $A$ 上幺半群，亦可使用这一单射性定律进行有效推导——此即代数中所谓的恒等永存性原理。此类性质对于设计并实现如 Lean 和 Coq 等计算机化证明助手的逻辑学家与计算机科学家具有根本性的实践重要性，因为它们使得方程问题的形式化归约成为可能，进而使类型检查变得可操作。随着类型理论日益复杂，建立其自由模型的有用性质（这些性质是有效实现的关键）也愈发困难。这些障碍促使了类型理论基础研究的回归，其几何化色彩比以往任何时候都更为浓厚。本文展示了一种现代方法，用以证明马丁-洛夫类型论自由模型的高度非平凡单射性定律，并特别关注格罗滕迪克学派的三个重要思想如何影响当代类型理论方法：相对观点、宇宙语言以及广义空间的粘合。