no goals
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
trans : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows
simpa using trans (𝟙 _)