transport has_limits w.r.t. equivalence

Stream: Is there code for X?

[Adam Topaz]

Does mathlib know the following fact? If $C$ and $D$ are equivalent categories, and $C$ has (co)limits then $D$ has (co)limits.

[Johan Commelin]

This should be something like equivalence.preserves_limits

[Johan Commelin]

Ooh, that's not exactly it. I guess "creates limits"?

[Adam Topaz]

Yeah, we should have the fact that equivalences create limits.

[Adam Topaz]

But it seems like that's missing too. at least I can't find it.

[Adam Topaz]

I wanted this because I was going to make the has_limits/has_colimits instances for simplicial sets, but there were some stupid universe issues and I wanted to use the skeletal equivalence.

[Scott Morrison]

Eek. I'm not finding it either. @Bhavik Mehta?

[Scott Morrison]

(deleted)

[Scott Morrison]

#6687

[Bhavik Mehta]

docs#category_theory.adjunction.is_equivalence_creates_limits

[Bhavik Mehta]

It was already there

[Scott Morrison]

Oh, and even easier.

[Scott Morrison]

Scaling problems...

[Bhavik Mehta]

I think lots of the lemmas in that file can be hard to find, perhaps we should add something to the docstrings about them

[Bhavik Mehta]

Actually maybe it's sensible to move that file to limits.adjunction and possibly split some things off into limits.equivalence

[Adam Topaz]

Thanks @Bhavik Mehta I'm adding a def for transporting has_(co)limits instances across an equivalence.