Transporting properties along an equivalence of cats

Stream: Is there code for X?

[Fernando Chu]

Is there an easy way to transport properties along an equivalence of cats? Specifically I'm working with ThinSkeleton C, and I was hoping there's an easy way to, say, ThinSkeleton C has colimits when C also has them, etc.

I could add an instance saying that ThinSkeleton inherits colimits, but given that there are quite a huge number of possible properties of C, I'm wondering if there's a better way (in my use case I only care about like 4 properties, though).

[Aaron Liu]

@loogle CategoryTheory.Equivalence, "colimit"

[loogle]

:search: CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence, CategoryTheory.Limits.IsColimit.whiskerEquivalence, and 24 more

[Adam Topaz]

This is a general issue that comes up a lot. In this case, an equivalence is a functor that creates colimits, and whenever you have such a functor and the target category has colimits then so does the source. See hasColimits_of_hasColimits_createsColimits (… I think)

[Adam Topaz]

More generally its possible to transport structure across some functor with some property that’s weaker than being an equivalence (e.g. sometimes you just need an adjunction!) and that is usually how we phrase things in mathlib

[Fernando Chu]

I see, thanks for the explanation. For my use case then, would you suggest creating an instance like HasColimits C -> HasColimits (ThinSkeleton C), or should I just state this for my very specific C?

[Adam Topaz]

That instance may be worthwhile to add (and same goes for HasLimits and for the weaker assertions in terms of having (co)limits of certain shapes)

[Fernando Chu]

Alright, thanks!