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