J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
s t : Cocone F
h : IsColimit t
f f' g : t ⟶ s
⊢ g = descCoconeMorphism 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 : Cocone F
h : IsColimit t
f f' : t ⟶ s
⊢ ∀ {g : t ⟶ s}, g = descCoconeMorphism h s
intro g
case w
J : Type u₁
inst : Category J
K : Type u₂
inst_1 : Category K
C : Type u₃
inst_2 : Category C
F : J ⥤ C
s t : Cocone F
h : IsColimit t
f f' g : t ⟶ s
⊢ g.Hom = desc 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 : Cocone F
h : IsColimit t
f f' g : t ⟶ s
⊢ g = descCoconeMorphism h s
aesop_cat_nonterminal
no goals
case w
J : Type u₁
inst : Category J
K : Type u₂
inst_1 : Category K
C : Type u₃
inst_2 : Category C
F : J ⥤ C
s t : Cocone F
h : IsColimit t
f f' g : t ⟶ s
⊢ g.Hom = desc h s
exact h.uniq _ _ g.w