module Cat.Functor.Equivalence.Complete where

Completeness respects equivalences🔗

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

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 C\mathcal{C} admits J\mathcal{J}-shaped limits, then for any diagram K:J→DK : \mathcal{J} \to \mathcal{D}, the composite F−1KF^{-1}K has a limit. But since equivalences are right adjoints, FF preserves this limit, so FF−1KFF^{-1}K has a limit in D\mathcal{D}; But that composite is naturally isomorphic to KK, so KK 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))))