Lemma indiscrete_topology_stability : Grothendieck_topology_stability_ax indiscrete_topology_selection. Proof. intros X Y f S HS. apply (is_functor_z_iso_pointwise_if_z_iso _ _ (homset_property _)). apply (Pullback_of_z_iso (g := Subobject_mor S)). exact (nat_trafo_z_iso_if_pointwise_z_iso (homset_property _) _ HS). 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.