Computable cartesian closed categories

Stream: mathlib4

[Albus Dompeldorius]

I want to work with cartesian closed categories in a computable way, but everything in Mathlib.CategoryTheory.Closed.Cartesian is marked as noncomputable, even though it seems that almost all of the definitions are already computable. Is there a reason we can't remove the global noncomputable and mark the few noncomputable definitions instead?

There are four noncomputable definitions:

def internalizeHom (f : A ⟶ Y) : ⊤_ C ⟶ A ⟹ Y

def powZero {I : C} (t : IsInitial I) [CartesianClosed C] : I ⟹ B ≅ 𝟙_ C

These can be made computable by replacing ⊤_ C with 𝟙_ C (which is available since we assume ChosenFiniteProducts C anyway).

def prodCoprodDistrib [HasBinaryCoproducts C] [CartesianClosed C] (X Y Z : C)

def cartesianClosedOfEquiv (e : C ≌ D) [CartesianClosed C] : CartesianClosed D :=
  letI := e.inverse.monoidalOfChosenFiniteProducts
  MonoidalClosed.ofEquiv (e.inverse) e.symm.toAdjunction

These remain noncomputable since they depend on the noncomputable HasBinaryCoproducts C MonoidalClosed.ofEquiv respectively.

[Kim Morrison]

No objection.

[Albus Dompeldorius]

Great! I will make a PR.

[Albus Dompeldorius]

Opened pull request here: PR.