Theorems · Theorem · category theory

CategoryTheory.Functor.CoconeTypes.IsColimit.of_equiv

∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes},
  c.IsColimit →
    ∀ {c' : F.CoconeTypes} (e : c.pt ≃ c'.pt), (∀ (j : J) (x : F.obj j), c'.ι j x = e (c.ι j x)) → c'.IsColimit

Defined in

Mathlib.CategoryTheory.Limits.Types.ColimitType

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category