Transporting existence of specific limits across equivalences

For now, we only treat the case of initial and terminal objects, but other special shapes can be added in the future.

theorem CategoryTheory.hasInitial_of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Functor D C) [e.IsEquivalence] [Limits.HasInitial C] : Limits.HasInitial D

theorem CategoryTheory.Equivalence.hasInitial_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : Limits.HasInitial C ↔ Limits.HasInitial D

theorem CategoryTheory.hasTerminal_of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Functor D C) [e.IsEquivalence] [Limits.HasTerminal C] : Limits.HasTerminal D

theorem CategoryTheory.Equivalence.hasTerminal_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : Limits.HasTerminal C ↔ Limits.HasTerminal D