Lemma indiscrete_topology_transitivity : Grothendieck_topology_transitivity_ax indiscrete_topology_selection. Proof. intros X S H. specialize (H X (identity X)). apply (is_functor_z_iso_pointwise_if_z_iso _ _ (homset_property _)). use (is_z_isomorphism_path _ (z_iso_is_z_isomorphism (indiscrete_topology_transitivity_iso H))). abstract ( apply nat_trans_eq_alt; intro Y; apply funextfun; intro x; apply id_right ). 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.