Lemma Grothendieck_topos_ind (P : category → hProp) (HP : ∏ (D : site), P (sheaf_cat D)) {C : category} (HU : is_univalent C) (HT : is_Grothendieck_topos C) : P C. Proof. revert HT. apply hinhuniv. exact (Grothendieck_topos_rect P HP HU). Qed.
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.