Lemma 48, p. 39 — concrete presheaves on a concrete site are separated

Let $D$ be a small category with a coverage $K$ and a terminal object $T$ (written $1$ in the paper), and suppose $(D,K,T)$ is a concrete site: representables are sheaves, $\operatorname{hom}(1,-)$ is faithful, and covering families are jointly surjective on points. Write $\underline{X}=X(1)$ for the underlying set of a presheaf $X$ and $\underline{\varphi}:\underline{D}\to\underline{X}$, $d\mapsto X(d)(\varphi)$, for the underlying function of a plot $\varphi\in X(D)$.

A presheaf $P$ is separated if, for every covering family $(f_i:D_i\to D)$, two plots $\varphi,\varphi'\in P(D)$ with $P(f_i)\varphi=P(f_i)\varphi'$ for all $i$ are equal. If $P$ is concrete, then

Consequently sheafification of a concrete presheaf needs only one application of the plus construction.

Formalization Note The site is small ($D$ in universe $u$, presheaves valued in $\mathrm{Type}_u$), covering families are presieves, and the terminal domain is passed explicitly as $(T, h_T)$. Separatedness is Mathlib's Presieve.IsSeparatedFor on each covering presieve of the coverage.