Generalise `limit.lift_self_id` etc to cones.

[EdAyers]

• limit.lift_self_id
• pullback.lift_self_id
• pullback.with_id_l
• pullback.comp_l it's a corol of Bhavik's pasting lemma

[b-mehta]

For with_id_l, here's what the type could look like

lemma pullback.with_id_l' {X Y : C} (f : X ⟶ Y) :
  is_limit (pullback_cone.mk f (𝟙 X) (show f ≫ (𝟙 Y) = (𝟙 X) ≫ f, by simp)) :=