C : Type u
inst✝⁴ : Category C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category D
inst✝² : ConcreteCategory D
inst✝¹ : PreservesLimits (forget D)
X : C
P : Cᵒᵖ ⥤ D
S : GrothendieckTopology.Cover J X
inst✝ : HasMultiequalizer (GrothendieckTopology.Cover.index S P)
x : Meq P S
I : GrothendieckTopology.Cover.Arrow S
⊢ ↑(↑(equiv P S) (↑(equiv P S).symm x)) I = ↑x I
C : Type u
inst✝⁴ : Category C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category D
inst✝² : ConcreteCategory D
inst✝¹ : PreservesLimits (forget D)
X : C
P : Cᵒᵖ ⥤ D
S : GrothendieckTopology.Cover J X
inst✝ : HasMultiequalizer (GrothendieckTopology.Cover.index S P)
x : Meq P S
I : GrothendieckTopology.Cover.Arrow S
⊢ (forget D).map (Multiequalizer.ι (GrothendieckTopology.Cover.index S P) I) (↑(equiv P S).symm x) = ↑x I
rw [← equiv_apply]
no goals
C : Type u
inst✝⁴ : Category C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category D
inst✝² : ConcreteCategory D
inst✝¹ : PreservesLimits (forget D)
X : C
P : Cᵒᵖ ⥤ D
S : GrothendieckTopology.Cover J X
inst✝ : HasMultiequalizer (GrothendieckTopology.Cover.index S P)
x : Meq P S
I : GrothendieckTopology.Cover.Arrow S
⊢ ↑(↑(equiv P S) (↑(equiv P S).symm x)) I = ↑x I
simp