Lemma sheaf_property_equalizer_inducer_arrow_commutes : (sheaf_property_equalizer_arrow1 ∘ sheaf_property_equalizer_inducer_arrow = sheaf_property_equalizer_arrow2 ∘ sheaf_property_equalizer_inducer_arrow)%functions. Proof. apply (ProductArrow_eq _ SET). intro VWfg. refine (assoc' _ _ _ @ _). refine (maponpaths _ (ProductPrCommutes _ _ _ _ _ _ _) @ _). refine (ProductPrCommutes _ _ _ _ _ _ (pr12 VWfg ,, _) @ !_). refine (assoc' _ _ _ @ _). refine (maponpaths _ (ProductPrCommutes _ _ _ _ _ _ _) @ _). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (ProductPrCommutes _ _ _ _ _ _ _) @ !_). refine (_ @ functor_comp _ _ _). apply maponpaths. exact (eqtohomot (nat_trans_ax (sieve_nat_trans S) _ _ _) _). 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.