## Stream: Is there code for X?

### Topic: transport has_limits w.r.t. equivalence

#### Adam Topaz (Mar 15 2021 at 04:04):

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 (Mar 15 2021 at 04:10):

This should be something like equivalence.preserves_limits

#### Johan Commelin (Mar 15 2021 at 04:10):

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

#### Adam Topaz (Mar 15 2021 at 04:12):

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

#### Adam Topaz (Mar 15 2021 at 04:13):

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

#### Adam Topaz (Mar 15 2021 at 04:13):

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 (Mar 15 2021 at 06:10):

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

(deleted)

#6687

#### Scott Morrison (Mar 15 2021 at 11:31):

Oh, and even easier.

#### Scott Morrison (Mar 15 2021 at 11:31):

Scaling problems...

#### Bhavik Mehta (Mar 15 2021 at 11:34):

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 (Mar 15 2021 at 12:33):

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

#### Adam Topaz (Mar 15 2021 at 14:16):

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

Last updated: May 19 2021 at 02:10 UTC