C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Initial F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cone G
P : IsLimit t
⊢ 𝟙 t.pt ≫ IsLimit.lift P (extendCone.obj (Cone.whisker F t)) = 𝟙 t.pt
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Initial F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cone G
P : IsLimit t
⊢ IsLimit.lift (↑(isLimitWhiskerEquiv F t).symm P) (Cone.whisker F t) = 𝟙 t.pt
change 𝟙 t.pt ≫ P.lift (extendCone.obj (Cone.whisker F t)) = 𝟙 t.pt
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Initial F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cone G
P : IsLimit t
⊢ ∀ (j : D), (𝟙 t.pt ≫ IsLimit.lift P (extendCone.obj (Cone.whisker F t))) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Initial F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cone G
P : IsLimit t
⊢ 𝟙 t.pt ≫ IsLimit.lift P (extendCone.obj (Cone.whisker F t)) = 𝟙 t.pt
apply P.hom_ext
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Initial F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cone G
P : IsLimit t
j : D
⊢ (𝟙 t.pt ≫ IsLimit.lift P (extendCone.obj (Cone.whisker F t))) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Initial F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cone G
P : IsLimit t
⊢ ∀ (j : D), (𝟙 t.pt ≫ IsLimit.lift P (extendCone.obj (Cone.whisker F t))) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j
intro j
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Initial F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cone G
P : IsLimit t
j : D
⊢ (𝟙 t.pt ≫ IsLimit.lift P (extendCone.obj (Cone.whisker F t))) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j
simp