J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
⊢ Cocone.extend (colimitCocone h) (homOfCocone h (coconeOfHom h (homOfCocone h s))) = coconeOfHom h (homOfCocone h s)
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
⊢ Cocone.extend (colimitCocone h) (homOfCocone h s) = s
rw [← coconeOfHom_homOfCocone h s]
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
⊢ Cocone.extend (colimitCocone h) (homOfCocone h s) = coconeOfHom h (homOfCocone h s)
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
⊢ Cocone.extend (colimitCocone h) (homOfCocone h (coconeOfHom h (homOfCocone h s))) = coconeOfHom h (homOfCocone h s)
conv_lhs => simp only [homOfCocone_cooneOfHom]
no goals
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
⊢ Cocone.extend (colimitCocone h) (homOfCocone h s) = coconeOfHom h (homOfCocone h s)
apply (coconeOfHom_fac _ _).symm