case w
C : Type u₁
inst✝² : Category C
J : Type u
inst✝¹ : Category J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝
C : Type u₁
inst✝² : Category C
J : Type u
inst✝¹ : Category J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F) = 𝟙 (limit F)
ext
no goals
case w
C : Type u₁
inst✝² : Category C
J : Type u
inst✝¹ : Category J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝
simp
no goals
C : Type u₁
inst✝² : Category C
J : Type u
inst✝¹ : Category J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.lift F (coneOfDiagramInitial I F) ≫ limit.π F j = 𝟙 (F.obj j)
simp