## 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
{"ft_lang_label":"__label__en","ft_lang_prob":0.9054469,"math_prob":0.47067273,"size":1804,"snap":"2021-21-2021-25","text_gpt3_token_len":554,"char_repetition_ratio":0.20166667,"word_repetition_ratio":0.1305842,"special_character_ratio":0.32815966,"punctuation_ratio":0.17091836,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9513704,"pos_list":[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24],"im_url_duplicate_count":[null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-05-19T02:34:23Z\",\"WARC-Record-ID\":\"<urn:uuid:8d00f1df-2301-4023-82dd-433f49d8a2a2>\",\"Content-Length\":\"17382\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:02c12b29-e9e5-47af-af52-f7a6a75af8fe>\",\"WARC-Concurrent-To\":\"<urn:uuid:3dbcdbcc-77cd-4d53-b396-6e7d6799e4d8>\",\"WARC-IP-Address\":\"185.199.111.153\",\"WARC-Target-URI\":\"https://leanprover-community.github.io/archive/stream/217875-Is-there-code-for-X%3F/topic/transport.20has_limits.20w.2Er.2Et.2E.20equivalence.html\",\"WARC-Payload-Digest\":\"sha1:TAO7IJ3YX7Z6GV2PNQGXMNMF2EKDA4LB\",\"WARC-Block-Digest\":\"sha1:7JG5CH7PHZP2MR7EUKEGZXPWMSF3BT5B\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-21/CC-MAIN-2021-21_segments_1620243991562.85_warc_CC-MAIN-20210519012635-20210519042635-00461.warc.gz\"}"}