Lemma Grothendieck_topos_rect (P : category → UU) (HP : ∏ (D : site), P (sheaf_cat D)) {C : category} (HU : is_univalent C) (HT : Grothendieck_topos_structure C) : P C. Proof. refine (transportf P _ (HP (Grothendieck_topos_structure_site HT))). apply (invmap (catiso_is_path_cat _ _)). use (adj_equivalence_of_cats_to_cat_iso (adj_equivalence_of_cats_inv _ (Grothendieck_topos_structure_equiv HT))). - apply sheaf_cat_univalent. - apply 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.