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
S : Sieve X
x : FamilyOfElements P S.arrows
t : Compatible x
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ x (g ≫ f) (_ : S.arrows (g ≫ f)) = P.map g.op (x f hf)
simpa using t (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)