does CCC preserve category equivalence

Stream: maths

[Kenny Lau]

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

[Kenny Lau]

(CCC = Cartesian Closed Category)

[Bhavik Mehta]

Yup, this is in mathlib already :)

[Bhavik Mehta]

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

[Kenny Lau]

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]

Sure, but I don't have the latter yet

[Bhavik Mehta]

And I've done the former

[Bhavik Mehta]

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

[Kenny Lau]

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

[Bhavik Mehta]

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

[Kenny Lau]

oops

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Kenny Lau]

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

[Bhavik Mehta]

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]

do we know that empty and 1 are CCCs?

[Bhavik Mehta]

We don't have any CCCs in mathlib right now

[Kenny Lau]

then maybe I can PR the empty case

[Kenny Lau]

(is empty a category?)

[Bhavik Mehta]

Yeah, it's called pempty

[Kenny Lau]

ok I'll work on the pempty case

[Bhavik Mehta]

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

[Kenny Lau]

failed to synthesize type class instance for
⊢ category pempty

[Kenny Lau]

which file should I import?

[Bhavik Mehta]

category_theory.pempty, I think

[Kenny Lau]

oh no pempty is not CCC

[Kenny Lau]

guess why

[Bhavik Mehta]

oh terminal doesn't exist

[Kenny Lau]

bingo

[Kenny Lau]

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,
  { is_adj :=
    { right := { obj := id, map := λ _ _, id },
      adj :=
      { hom_equiv := λ _ _, equiv.refl punit,
        unit := { app := id },
        counit := { app := id } } } } }

end category_theory

[Kenny Lau]

yay

[Bhavik Mehta]

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

[Kenny Lau]

:octopus: