module Cat.Functor.Equivalence.Complete where

Completeness respects equivalences🔗

Let be a category admitting limits for diagrams, and an equivalence. Then also admits limits for diagrams; In particular, if is complete, then so is

  _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
    {F : Functor C D} (eqv : is-equivalence F)

  open is-equivalence eqv

This is a very short theorem: If admits limits, then for any diagram the composite has a limit. But since equivalences are right adjoints, preserves this limit, so has a limit in But that composite is naturally isomorphic to so also has a limit.

  equivalence→complete : ∀ {co cℓ} → is-complete co cℓ C → is-complete co cℓ D
  equivalence→complete ccomp K =
    natural-iso→limit (F∘-iso-id-l F∘F⁻¹≅Id)
      (subst Limit F∘-assoc (right-adjoint-limit F⁻¹⊣F (ccomp (F⁻¹ F∘ K))))