Definition Grothendieck_topos_structure (C : category) : UU := ∑ (D : site), adj_equiv C (sheaf_cat D).
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.