case h
C : Type u_4
inst✝⁴ : Category C
D : Type u_2
inst✝³ : Category D
E : Type ?u.66083
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.66135
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : Functor.op G ⋙ ℱ ⟶ Functor.op G ⋙ ℱ'.val
X : D
Y : C
f : X.op ⟶ (G.obj Y).op
a✝ : ℱ.obj X.op
⊢ (appHom H α X ≫ ℱ'.val.map f) a✝ = (ℱ.map f ≫ α.app Y.op) a✝
C : Type u_4
inst✝⁴ : Category C
D : Type u_2
inst✝³ : Category D
E : Type ?u.66083
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.66135
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : Functor.op G ⋙ ℱ ⟶ Functor.op G ⋙ ℱ'.val
X : D
Y : C
f : X.op ⟶ (G.obj Y).op
⊢ appHom H α X ≫ ℱ'.val.map f = ℱ.map f ≫ α.app Y.op
ext
no goals
case h
C : Type u_4
inst✝⁴ : Category C
D : Type u_2
inst✝³ : Category D
E : Type ?u.66083
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.66135
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : Functor.op G ⋙ ℱ ⟶ Functor.op G ⋙ ℱ'.val
X : D
Y : C
f : X.op ⟶ (G.obj Y).op
a✝ : ℱ.obj X.op
⊢ (appHom H α X ≫ ℱ'.val.map f) a✝ = (ℱ.map f ≫ α.app Y.op) a✝
apply appHom_restrict