Lean4
/-- Given a cocone over `F ⋙ G`, we can construct a `Cocone G` with the same cocone point.
-/
@[simps]
def extendCocone : Cocone (F ⋙ G) ⥤ Cocone G
where
obj
c :=
{ pt := c.pt
ι :=
{ app := fun X => G.map (homToLift F X) ≫ c.ι.app (lift F X)
naturality := fun X Y f => by
dsimp;
simp only [Category.comp_id]
-- This would be true if we'd chosen `lift F X` to be `lift F Y`
-- and `homToLift F X` to be `f ≫ homToLift F Y`.
apply induction F fun Z k => G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k ≫ c.ι.app Z
· intro Z₁ Z₂ k₁ k₂ g a z
rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w, z]
· intro Z₁ Z₂ k₁ k₂ g a z
rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w] at z
rw [z]
· rw [← Functor.map_comp_assoc] } }
map f := { hom := f.hom }
