  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.
