materialization construction, defined categorically in . \[sec:matCat\], that enables us to concretize an instance of a left-hand side in a given abstract object. This construction is refined in . \[sec:matRew\] where we restrict to materializations that satisfy the gluing condition and can thus be rewritten via $p$. Finally in . \[sec:RewMat\] we present the main result about materializations showing that we can fully characterize the co-matches obtained by rewriting.

Materialization Category and Existence of Materialization {#sec:matCat}
---------------------------------------------------------

From now on we assume $\C$ to be an elementary topos.

\[def:materialization-category\] Let $\phi\colon L\to A$ be an arrow in $\C$.\
The *materialization category* for $\phi$, denoted $\matcat{\phi}$, has as

objects

:   all factorizations $L\rat X\to A$ of $\phi$ whose first factor $L\rat X$ is a mono, and as

arrows

:   from a factorization $L\rat X\to A$ to another one $L\rat Y\to A$, all arrows $f\colon X\to Y$ in $\C$ such that the diagram to the right comprises a commutative triangle and a pullback square.

$$\tikzsetnextfilename{arrowsOfMatCat}      \begin{tikzpicture}
        \node{\begin{tikzcd}[row sep=1ex] L
            \ar[tail,"\mathit{id}_L"',dd]             \ar[tail,r]             \ar[dotted,drr,"\phi",bend left=30,near end,shift left=1]
            & X \ar[dd,"f" description] \ar[dr]             \\
            && A
            \\
            L \ar[tail,r] \ar[rru,dotted,"\phi"',bend right=30,near
            end,shift right=1] & Y \ar[ur]
            \ar[uul,phantom,"\color{gray}\scriptstyle\mathrm{(PB)}"]
          \end{tikzcd}};
      \end{tikzpicture}$$

If has a terminal object it 