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.Functor.Base
open import Cat.Prelude

module Cat.Functor.Equivalence.Complete where

Completeness respects equivalencesπŸ”—

Let C\ca{C} be a category admitting limits for J\ca{J}-shaped diagrams, and F:C≅DF : \ca{C} \cong \ca{D} an equivalence. Then D\ca{D} also admits limits for J\ca{J}-shaped diagrams; In particular, if C\ca{C} is complete, then so is D\ca{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\ca{C} admits J\ca{J}-shaped limits, then for any diagram K:Jβ†’DK : \ca{J} \to \ca{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\ca{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 =
    Limit-ap-iso (F∘-iso-id-l F∘F⁻¹≅Id)
      (subst Limit F∘-assoc (right-adjoint-limit F⁻¹⊣F (ccomp (F⁻¹ F∘ K))))