module Cat.Functor.Equivalence.Complete where

# Completeness respects equivalences🔗

Let $C$ be a category admitting limits for $J-shaped$ diagrams, and $F:C≅D$ an equivalence. Then $D$ also admits limits for $J-shaped$ diagrams; In particular, if $C$ is complete, then so is $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$ admits $J-shaped$ limits, then for any diagram $K:J→D,$ the composite $F_{−1}K$ has a limit. But since equivalences are right adjoints, $F$ preserves this limit, so $FF_{−1}K$ has a limit in $D;$ But that composite is naturally isomorphic to $K,$ 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))))