is_iso_ι_of_forall_is_iso

Stream: Is there code for X?

[Adam Topaz]

Do we have the following?

import category_theory.limits.shapes.terminal

namespace category_theory.limits

open category_theory

universes v u
variables {J : Type v} [small_category J] {C : Type u} [category.{v} C] (F : J ⥤ C)

lemma colimit.is_iso_ι_of_forall_is_iso {j : J} (hj : is_initial j)
  [has_colimit F] [∀ (a b : J) (f : a ⟶ b), is_iso (F.map f)] :
  is_iso (colimit.ι F j) := sorry

end category_theory.limits

[Scott Morrison]

I think not.

[Adam Topaz]

Ok, I'll open a PR soon