open import Cat.Functor.Adjoint.Continuous
open import Cat.Functor.Equivalence
open import Cat.Diagram.Limit.Base
open import Cat.Instances.Functor
open import Cat.Prelude

module Cat.Functor.Equivalence.Complete where

Completeness respects equivalences🔗

Let $\mathcal{C}$ be a category admitting limits for $\mathcal{J}\text{-shaped}$ diagrams, and $F:\mathcal{C}\cong \mathcal{D}$ an equivalence. Then $\mathcal{D}$ also admits limits for $\mathcal{J}\text{-shaped}$ diagrams; In particular, if $\mathcal{C}$ is complete, then so is $\mathcal{D}\text{.}$

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

  open is-equivalence eqv

This is a very short theorem: If $\mathcal{C}$ admits $\mathcal{J}\text{-shaped}$ limits, then for any diagram $K:\mathcal{J}\to \mathcal{D}\text{,}$ the composite $F^{-1}K$ has a limit. But since equivalences are right adjoints, $F$ preserves this limit, so $F{F}^{-1}K$ has a limit in $\mathcal{D}\text{;}$ But that composite is naturally isomorphic to $K\text{,}$ so $K$ 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))))