Lemma is_sheaf_to_is_sheaf' : is_sheaf → is_sheaf'. Proof. intros H c S. specialize (H c S). use (make_is_z_isomorphism _ _ (make_dirprod _ _)). - intro fH. refine (pr11 (H _) _ (identity c)). use make_nat_trans. * intros d f. refine (pr1 fH (d ,, f)). * abstract ( intros d d' f; apply funextfun; intro g; exact (eqtohomot (pr2 fH) (make_sheaf_property_equalizer_codomain_index _ (make_sieve_selected_morphism _ _) _ _)) ). - apply funextfun. intro x. use (!eqtohomot (nat_trans_eq_pointwise (path_to_ctr _ _ (H _) (make_nat_trans _ _ _ _) _) _) _ @ _). + intros d g. refine (# P g x). + intros d d' g. apply funextfun. intro g'. exact (eqtohomot (functor_comp P g' g) x). + apply nat_trans_eq_alt. reflexivity. + exact (eqtohomot (functor_id P c) x). - apply funextfun. intro w. apply subtypePath. { intro. apply impred_isaset. intro. apply setproperty. } apply funextsec. intro f. refine (!eqtohomot (nat_trans_ax (pr11 (H _)) _ _ _) _ @ _). refine (maponpaths (pr11 (H _) _) (id_right _) @ _). exact (eqtohomot (nat_trans_eq_pointwise (pr21 (H _)) _) _). 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.