Lemma is_sheaf''_to_is_sheaf : is_sheaf'' → is_sheaf. Proof. intros H X S t. induction H as [HL HG]. specialize (HG X S (λ f, t _ (sieve_selected_morphism_preimage f)) (λ f Z g, eqtohomot (nat_trans_ax t _ _ g) _)). use unique_exists. - apply (invmap (yoneda_weq C X P)). exact (pr1 HG). - apply nat_trans_eq_alt. intro Y. apply funextfun. intro x. exact (pr2 HG (make_sieve_selected_morphism (S := S) Y x)). - intro y. apply (homset_property (PreShv C)). - intros f Hf. apply pathsweq1. apply (HL X S). intro g. refine (_ @ !pr2 HG g). refine (!eqtohomot (nat_trans_ax f _ _ _) _ @ _). refine (_ @ eqtohomot (nat_trans_eq_weq (homset_property _) _ t Hf _) _). apply (maponpaths (f _)). apply id_right. 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.