J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g = liftConeMorphism h s
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' : s ⟶ t
⊢ ∀ {g : s ⟶ t}, g = liftConeMorphism h s
intro g
case w
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g.Hom = (liftConeMorphism h s).Hom
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g = liftConeMorphism h s
apply ConeMorphism.ext
no goals
case w
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g.Hom = (liftConeMorphism h s).Hom
exact h.uniq _ _ g.w