Definition sheaf_glueing_ax : UU := ∏ (c : C) (S : covering_sieve c) (x : ∏ (f : sieve_selected_morphism S), (P (sieve_selected_morphism_domain f) : hSet)), (∏ (f : sieve_selected_morphism S) (W : C) (g : C⟦W, sieve_selected_morphism_domain f⟧), x (sieve_selected_morphism_compose f g) = # P g (x f)) → ∑ (z : P c : hSet), ∏ (f : sieve_selected_morphism S), # P f z = x f.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.FullSubcategory. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sieves. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sites.