C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f = (colimitObjIsoColimitCompEvaluation H k).inv ≫ g
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ f = g
apply (cancel_epi (colimitObjIsoColimitCompEvaluation H k).inv).1
case w
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
j : J
⊢ colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f =
    colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ g
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f = (colimitObjIsoColimitCompEvaluation H k).inv ≫ g
ext j
no goals
case w
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
j : J
⊢ colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f =
    colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ g
simpa using w j