Category theory: mapping cones

Stream: Is there code for X?

[Jon Eugster]

Does the statement that G.mapCone c ≅ G.mapCone d from c ≅ d already exist somewhere?

import Mathlib

universe v₁ u₁ w v' v u u'

open CategoryTheory Limits in
def helper
    {J : Type u₁} [Category.{v₁} J]
    {V : Type u'} [Category.{v'} V]
    {C : Type u} [Category.{v} C]
    {F : J ⥤ C} {c d : Cone F} {G : C ⥤ V} (h : c ≅ d) :
    G.mapCone c ≅ G.mapCone d :=
  sorry

[Junyan Xu]

(Cones.functoriality ..).mapIso h

[Jon Eugster]

thanks :)