module Cat.Functor.Equivalence.Complete where
Completeness respects equivalencesπ
Let be a category admitting limits for -shaped diagrams, and an equivalence. Then also admits limits for -shaped diagrams; In particular, if is complete, then so is .
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 admits -shaped 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))))