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$ 下幺半群的形式理论中进行推理时，即使对于标量乘法非单射的幺半群，也可以利用这一单射律进行合理演绎——这一原则在代数中被称为“恒等式的持久性”。这类性质对设计和实现像 Lean 和 Coq 这样的计算机化证明助手的逻辑学家和计算机科学家具有根本性的实际重要性，因为它们使得方程问题的形式化简成为可能，从而让类型检查变得可处理。随着类型理论日益复杂，确立其自由模型的有用性质（这些性质对有效实现至关重要）也变得越来越困难。这些障碍促使类型理论的基础研究重新焕发活力，并呈现出前所未有的几何化趋势。本文展示了一种现代方法，用于证明马丁-洛夫类型理论自由模型的高度非平凡单射律，并特别关注格罗滕迪克学派三个重要思想——相对视点、宇宙语言和广义空间的粘合——如何影响当代类型理论方法。