Definition Grothendieck_topos_structure_equiv {C : category} (G : Grothendieck_topos_structure C) : adj_equiv C (sheaf_cat (Grothendieck_topos_structure_site G)) := pr2 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.