Category of Cartesian closed categories

Stream: mathlib4

[Chris Henson]

As far as I know, we don't currently have the category of ccc's in mathlib. If I'm overlooking it or maybe it's been done in another project, I'd appreciate it being pointed out.

For docs#CategoryTheory.Cat, we work with a structure that bundles the objects. Would it make sense to do something similar for ccc's? My first thought is that you would need to bundle the additional typeclass instances (i.e. Category and Limits.HasFiniteProducts).

[Chris Henson]

Following up, I almost have this done. The one proof I have left and am struggling with a bit is that CartesianClosedFunctor composes. Here's how far I got:

import Mathlib

open CategoryTheory Limits

variable (X : Type) [Category X] [HasFiniteProducts X] [CartesianClosed X]
variable (Y : Type) [Category Y] [HasFiniteProducts Y] [CartesianClosed Y]
variable (Z : Type) [Category Z] [HasFiniteProducts Z] [CartesianClosed Z]
variable (F : X ⥤ Y) (G : Y ⥤ Z)
variable  [PreservesLimitsOfShape (Discrete WalkingPair) F] [PreservesLimitsOfShape (Discrete WalkingPair) G]
variable [CCF_F : CartesianClosedFunctor F] [CCF_G : CartesianClosedFunctor G]

lemma compCartesianClosedFunctor : CartesianClosedFunctor (F ⋙  G) := by
  refine {comparison_iso := ?_ }
  intros A
  -- right type, but a bit unsure if this is correct...
  obtain ⟨inv_F, ⟨F_inv_r,F_inv_l⟩⟩ := (CCF_F.comparison_iso A).out
  obtain ⟨inv_G, ⟨G_inv_r,G_inv_l⟩⟩ := (CCF_G.comparison_iso (F.obj A)).out
  exists rightAdjointSquare.hcomp inv_G inv_F
  sorry

Is this headed in the right direction?

[Johan Commelin]

Sorry for only responding to this thread now...
@Sina H 𓃵 you have CCC's right? Or only LCCC's?

[Chris Henson]

No worries! I've seen LCCCs in the polynomial functor repo, but I don't think CCCs? I'm working on categorical semantics for polymorphism and dependent types, so I'll need both.

[Sina Hazratpour 𓃵]

@Chris Henson Completely missed this! sorry, not good with Zulip! CCCs were already in mathlib before LCCCs in Mathlib.CategoryTheory.Closed.Cartesian
And LCCCs are now in a branch that is in the PR review #21525

[Sina Hazratpour 𓃵]

But to answer your question, i think we don't have a category/2-category of CCCs or LCCCs in mathlib. In Poly project you cited, there is a category and bicategory of polynomial functors but morphims are not CartesianClosedFunctor.

I think it would be nice to have category (or 2-category) of CCCs and LCCCs.
This would be a categorification of the category of Heyting algebras with homs defined by HeytingHom. Also, it would be give a basis for later obtaining a category of elementary toposes where the homs are defined by logical mophisms which are basically CartesianClosedFunctor.

Can you say a few words about the context of your project?