Definition site_stability {X Y : C} (f : Y --> X) {S : sieve X} (H : site_topology X S) : site_topology Y (sieve_pullback f S) := Grothendieck_topology_stability _ _ _ _ _ H.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sieves. Require Import UniMath.CategoryTheory.GrothendieckToposes.Topologies.