Definition Grothendieck_topos_structure_site {C : category} (G : Grothendieck_topos_structure C) : site := pr1 G.
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.Core.Univalence. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sheaves. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sites.