J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
⊢ Cone.extend (limitCone h) (homOfCone h (coneOfHom h (homOfCone h s))) = coneOfHom h (homOfCone h s)
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
⊢ Cone.extend (limitCone h) (homOfCone h s) = s
rw [← coneOfHom_homOfCone h s]
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
⊢ Cone.extend (limitCone h) (homOfCone h s) = coneOfHom h (homOfCone h s)
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
⊢ Cone.extend (limitCone h) (homOfCone h (coneOfHom h (homOfCone h s))) = coneOfHom h (homOfCone h s)
conv_lhs => simp only [homOfCone_coneOfHom]
no goals
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
⊢ Cone.extend (limitCone h) (homOfCone h s) = coneOfHom h (homOfCone h s)
apply (coneOfHom_fac _ _).symm