Sheafification exists for the fppf site

Size of the fixed site and its coverings. The category $\mathcal{C}$ is small in the sense of Category, object, morphism, domain, codomain, identity, composition, and hom-collection: its object and arrow collections are sets. Such a set-category closed under fibre products can be obtained from any set of required $S$-schemes by including $S$ and the empty scheme and repeatedly adjoining one fibre product for each pair of arrows with common target. At each finite stage there are only set-many pairs, because morphisms between two schemes form a set; AC selects the fibre-product models for the set of pairs at each stage, and the union of these stages is a set and contains fibre products for every pair of its arrows. This construction verifies the size and closure properties used here; a saturated bounded big site as in the cited Stacks construction has these same properties. For fixed $T$, the arrows with target $T$ form a set $M_T$. Replace a covering family by its support, the subset of $M_T$ consisting of the distinct arrows occurring in it. Its support is still a cover. Repeated occurrences of an arrow carry identical sections in a matching family: pull their compatibility equality back along the diagonal of its source over $T$. Hence deleting repetitions neither changes the matching-family set nor the generated sieve. Covering supports thus form a subset of $\mathcal{P}(M_T)$, and the sieves they generate also form a set. All products of section sets and all colimits below are therefore small. No existence axiom for Grothendieck universes is used.

The plus construction. For a covering $U=\{T_i\to T{\}}_{i\in I}$ let $E_F(U)$ be the set of compatible families in ${\prod }_{i}F(T_i)$. Order coverings by refinement, so that arrows go from a covering to a refining covering. A refinement pulls a matching family back, independently of the chosen refinement maps: two maps from a member $V$ to members $T_i,T_j$ over $T$ give a map $V\to T_i{\times }_T{T}_j$, and compatibility makes the two restrictions equal. Thus $E_F$ is a functor on the preorder of coverings, even though the category retaining all refinement maps need not be filtered. The preorder is filtered by the common product refinement of [F1]. Use the covering supports of step 1.1. Refinement of supports is a preorder on a set; their product refinement is again a covering support after removing repetitions. Thus its filtered colimit is a colimit over a small category. Define $F^{+}(T)={\mathrm{colim}}_U{E}_F(U)$. The identity covering supplies $F(T)\to F^{+}(T)$; base change of coverings defines restriction maps. Independence of refinement maps and [F1] give the presheaf identities and naturality of this unit. For the empty target the empty covering has a singleton matching set; it refines every covering, so $F^{+}(\mathrm{\varnothing })$ is a singleton.

The plus construction is universal for maps into sheaves. Given $a:F\to H$ with $H$ a sheaf, apply $a$ to a compatible family representing an element of $F^{+}(T)$ and glue in $H(T)$. Refinement does not change the glued element, because its restrictions agree on a covering; equality in the filtered colimit is eventual by [F4]. This defines a natural extension $F^{+}\to H$. It is unique: every element of $F^{+}$ is locally the image of its representing sections of $F$, and the sheaf condition determines its image in $H$.

$F^{+}$ is separated. Suppose $x,y\in F^{+}(T)$ agree on every member $T_i$ of a covering. Choose a common refinement of their representative coverings. On each $T_i$, [F4] gives a further covering where the two restricted matching families agree. AC chooses these witnesses for the set of indices $i$, and [F1] composes all these local refinements into one covering of $T$ on which the representatives agree. Therefore $x=y$ by [F4]. Moreover the unit $G\to G^{+}$ is injective for every separated presheaf $G$: equality of two unit images is equality on a covering, hence equality in $G$.

Separated presheaves have sheafified plus. Let $G$ be separated and let $x_i\in G^{+}(T_i)$ be a matching family. Using AC, represent each $x_i$ on a covering $\{T_{ij}\to T_i\}$ by a matching family $s_{ij}\in G(T_{ij})$. On $W=T_{ij}{\times }_T{T}_{i^{\mathrm{\prime }}{j}^{\mathrm{\prime }}}$, the images of the two restricted sections in $G^{+}(W)$ agree, since both represent the restrictions of the matching $x_i,x_{i^{\mathrm{\prime }}}$. Injectivity of $G(W)\to G^{+}(W)$ from step 3.2 makes the sections themselves equal. Thus $(s_{ij})$ is a matching family on the composed covering of $T$; its class in $G^{+}(T)$ glues the $x_i$. Uniqueness follows from the separatedness of $G^{+}$ in step 3.2. Consequently $G^{+}$ is a sheaf. AC is used to select local representatives here and local equality witnesses in step 3.2; it never asserts that the category of all refinement maps is filtered.

Sheafification. By step 3.2 $F^{+}$ is separated, and by step 4.1 $F^{++}$ is a sheaf. Applying step 3.1 twice proves that $F\to F^{++}$ is universal for maps into sheaves. It is unique up to unique isomorphism by [F2]. If $F$ is already a sheaf, gluing its matching families identifies $F^{+}(T)$ with $F(T)$ for every $T$, compatibly with restriction, so the unit to $F^{++}$ is an isomorphism. A natural transformation acts on matching families, hence on their colimits, proving functoriality.

Finite limits. For a fixed covering $U$, the functor $F\mapsto E_F(U)$ commutes with all limits: a matching family in an objectwise limit is exactly a coherent collection of matching families in its component presheaves, because the two compatibility equalities can be tested componentwise. This argument permits infinite covering families; it does not require the products defining $E_F(U)$ to be finite. For a finite diagram of presheaves, its components use the same filtered preorder of coverings of $T$, so [F3] interchanges its finite limit with the filtered colimit in step 2.1. Thus plus, and then double plus, commutes with finite limits. Finite limits of sheaves are computed objectwise, since compatible local sections in each component glue uniquely and their diagram identities follow by local uniqueness. This proves the asserted finite-limit property of sheafification.