Lemma indiscrete_presheaf_is_sheaf {C : category} (P : PreShv C) : is_sheaf (indiscrete_site C) P. Proof. intros X S f. refine ((_ : is_iso (C := PreShv C) _) _ f). apply is_iso_from_is_z_iso. apply nat_trafo_z_iso_if_pointwise_z_iso. exact (pr2 S). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.Subobjects. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sheaves. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sieves. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sites. Require Import UniMath.CategoryTheory.GrothendieckToposes.Topologies.