Definition Grothendieck_topology_transitivity_ax : hProp := ∀ (c : C) (s : sieve c), (∏ (c' : C) (h : c' --> c), selection c' (sieve_pullback h s)) ⇒ selection c s.
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.Monics. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.Subobjects. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sieves.