Definition site_maximal_sieve (X : C) : site_topology X (maximal_sieve X) := Grothendieck_topology_maximal_sieve _ _.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sieves. Require Import UniMath.CategoryTheory.GrothendieckToposes.Topologies.