Definition indiscrete_topology_transitivity_iso {X : C} {S : Sieves.sieve X} (H : is_nat_z_iso (sieve_nat_trans (PullbackSubobject Pullbacks_PreShv S (# (yoneda C) (identity X))))) : z_iso (Subobject_dom S) (yoneda C X). Proof. refine (z_iso_comp (b := Pullbacks_PreShv _ _ _ (# (yoneda C) (identity X)) (sieve_nat_trans S)) (z_iso_inv _) _). - refine (_ ,, _). apply Pullback_of_z_iso'. apply functor_on_is_z_isomorphism. apply is_z_isomorphism_identity. - refine (_ ,, _). apply (nat_trafo_z_iso_if_pointwise_z_iso (homset_property _)). exact H. 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.