case w.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G✝ G'✝ G G' : Subpresheaf F
h : G ≤ G'
x✝ : Cᵒᵖ
a✝ : (toPresheaf G).obj x✝
⊢ (homOfLe h ≫ ι G').app x✝ a✝ = (ι G).app x✝ a✝
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G✝ G'✝ G G' : Subpresheaf F
h : G ≤ G'
⊢ homOfLe h ≫ ι G' = ι G
ext
no goals
case w.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G✝ G'✝ G G' : Subpresheaf F
h : G ≤ G'
x✝ : Cᵒᵖ
a✝ : (toPresheaf G).obj x✝
⊢ (homOfLe h ≫ ι G').app x✝ a✝ = (ι G).app x✝ a✝
rfl