## Stream: maths

### Topic: does CCC preserve category equivalence

#### Kenny Lau (Jun 16 2020 at 04:10):

if C and D are equivalent categories and C is CCC, does it follow that D is also CCC?

#### Kenny Lau (Jun 16 2020 at 04:10):

(CCC = Cartesian Closed Category)

#### Bhavik Mehta (Jun 16 2020 at 04:11):

Yup, this is in mathlib already :)

#### Bhavik Mehta (Jun 16 2020 at 04:11):

https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/closed/cartesian.lean#L324

#### Kenny Lau (Jun 16 2020 at 04:11):

then your goal that Type u is CCC follows from a more general theorem that if C is CCC then C => Type u (the category of functors) is CCC

#### Bhavik Mehta (Jun 16 2020 at 04:11):

Sure, but I don't have the latter yet

#### Bhavik Mehta (Jun 16 2020 at 04:12):

And I've done the former

#### Bhavik Mehta (Jun 16 2020 at 04:12):

(Largely to make sure my definition of CCC made sense)

#### Kenny Lau (Jun 16 2020 at 04:12):

well but I think in mathlib we prove the most general things first

#### Bhavik Mehta (Jun 16 2020 at 04:12):

Also, C => Type u being CCC doesn't need C to be CCC

oops

#### Bhavik Mehta (Jun 16 2020 at 04:13):

Yeah and that's why I haven't made a PR yet :)

#### Bhavik Mehta (Jun 16 2020 at 04:13):

Oh actually I already have done that C^op => Type u is CCC

#### Kenny Lau (Jun 16 2020 at 04:14):

then you can deduce that C => Type u is CCC :P

#### Bhavik Mehta (Jun 16 2020 at 04:15):

it's a pretty horrible proof though - if we're going for the most general thing then really we should show C^op => Type u is comonadic over Type u, and the category of coalgebras over a CCC is CCC

#### Kenny Lau (Jun 16 2020 at 04:15):

do we know that empty and 1 are CCCs?

#### Bhavik Mehta (Jun 16 2020 at 04:15):

We don't have any CCCs in mathlib right now

#### Kenny Lau (Jun 16 2020 at 04:15):

then maybe I can PR the empty case

#### Kenny Lau (Jun 16 2020 at 04:15):

(is empty a category?)

#### Bhavik Mehta (Jun 16 2020 at 04:16):

Yeah, it's called pempty

#### Kenny Lau (Jun 16 2020 at 04:16):

ok I'll work on the pempty case

#### Bhavik Mehta (Jun 16 2020 at 04:18):

If you desperately want more examples I can post my presheaf category version for now

#### Kenny Lau (Jun 16 2020 at 04:22):

failed to synthesize type class instance for
⊢ category pempty


#### Kenny Lau (Jun 16 2020 at 04:22):

which file should I import?

#### Bhavik Mehta (Jun 16 2020 at 04:24):

category_theory.pempty, I think

#### Kenny Lau (Jun 16 2020 at 04:28):

oh no pempty is not CCC

guess why

#### Bhavik Mehta (Jun 16 2020 at 04:29):

oh terminal doesn't exist

bingo

#### Kenny Lau (Jun 16 2020 at 04:34):

import category_theory.closed.cartesian
import category_theory.punit

universe u

namespace category_theory

instance : limits.has_finite_products.{u u} punit :=
{ has_limits_of_shape := λ J _ _,
{ has_limit := λ F,
{ cone := { X := punit.star,
π := { app := λ X, punit.star } },
is_limit := { lift := λ s, punit.star } } } }

instance : cartesian_closed.{u u} punit :=
{ closed := λ X,
{ right := { obj := id, map := λ _ _, id },
{ hom_equiv := λ _ _, equiv.refl punit,
unit := { app := id },
counit := { app := id } } } } }

end category_theory


yay

#### Bhavik Mehta (Jun 16 2020 at 04:35):

But doesn't this follow from C => Type u being CCC? ;)

#### Kenny Lau (Jun 16 2020 at 04:35):

:octopus:

Last updated: May 06 2021 at 17:38 UTC