Definition make_is_Grothendieck_topology (H1 : Grothendieck_topology_maximal_sieve_ax) (H2 : Grothendieck_topology_stability_ax) (H3 : Grothendieck_topology_transitivity_ax) : is_Grothendieck_topology := H1 ,, H2 ,, H3.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.Subobjects. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sieves.