Lemma isaprop_glueing_ax (H : sheaf_locality_ax) : isaprop sheaf_glueing_ax. Proof. apply impred_isaprop. intro c. apply impred_isaprop. intro S. apply impred_isaprop. intro x. apply impred_isaprop. intro Hx. apply invproofirrelevance. intros z z'. apply subtypePath. { intro. repeat (apply impred_isaprop; intro). apply setproperty. } apply (H c S). intro f. exact (pr2 z _ @ !pr2 z' _). Qed.
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.