J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ c.ι.app j ≫ ((const J).obj c.pt).map f = c.ι.app j
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ c.ι.app j' = c.ι.app j
rw [c.ι.naturality f]
no goals
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ c.ι.app j ≫ ((const J).obj c.pt).map f = c.ι.app j
apply comp_id