# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Presheaves have all (co)limits

#### Adam Topaz (Dec 07 2020 at 16:54):

```
import category_theory.functor_category
import category_theory.limits.types
open category_theory
open category_theory.limits
variables (C : Type) [small_category C]
example : has_colimits (Cᵒᵖ ⥤ Type) := sorry -- Do we have this somewhere?
example : has_limits (Cᵒᵖ ⥤ Type) := sorry -- Do we have this somewhere?
```

#### Johan Commelin (Dec 07 2020 at 17:09):

@Bhavik Mehta :up:

#### Reid Barton (Dec 07 2020 at 17:11):

It's definitely somewhere

#### Reid Barton (Dec 07 2020 at 17:12):

for diagrams in any (co)complete category

#### Adam Topaz (Dec 07 2020 at 17:12):

Yeah, that's what I was expecting too, which is why the `import category_theory.limits.types`

import is there

#### Adam Topaz (Dec 07 2020 at 17:14):

```
import category_theory.functor_category
import category_theory.limits.types
import category_theory.limits.functor_category
open category_theory
open category_theory.limits
variables (C : Type) [small_category C]
example : has_colimits (Cᵒᵖ ⥤ Type) := by apply_instance
example : has_limits (Cᵒᵖ ⥤ Type) := by apply_instance
```

#### Adam Topaz (Dec 07 2020 at 17:14):

Got it!

#### Adam Topaz (Dec 07 2020 at 17:14):

`import category_theory.limits.functor_category`

was missing.

#### Adam Topaz (Dec 07 2020 at 17:15):

I don't presume the universal property of presheaves as being the free cocompletion is in mathlib?

#### Bhavik Mehta (Dec 07 2020 at 17:20):

Yup as Reid says this is in mathlib

#### Bhavik Mehta (Dec 07 2020 at 17:20):

@Adam Topaz It is, look in `ct/limits/presheaf`

iirc

#### Adam Topaz (Dec 07 2020 at 17:25):

For a little context.... I'd like to define `Ind C`

as the subcategory of `Cᵒᵖ ⥤ Type`

generated by filtered colimits of representables. @Reid Barton @Bhavik Mehta Any thoughts on whether this is a good idea?

#### Bhavik Mehta (Dec 07 2020 at 17:29):

My instinct is that this might get awkward but I don't know for sure, and off the top of my head I don't have better suggestions. You probably want to use `is_limit`

rather than isomorphisms with `limit`

though if you do go about it this way

Last updated: May 17 2021 at 16:26 UTC