feat: port CategoryTheory.Closed.Types (#4918)

Mathlib.lean

@@ -764,6 +764,7 @@ import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.CategoryTheory.Closed.Cartesian
 import Mathlib.CategoryTheory.Closed.FunctorCategory
 import Mathlib.CategoryTheory.Closed.Monoidal
+import Mathlib.CategoryTheory.Closed.Types
 import Mathlib.CategoryTheory.CofilteredSystem
 import Mathlib.CategoryTheory.CommSq
 import Mathlib.CategoryTheory.Comma

Mathlib/CategoryTheory/Closed/Cartesian.lean

@@ -78,6 +78,14 @@ abbrev CartesianClosed (C : Type u) [Category.{v} C] [HasFiniteProducts C] :=
   MonoidalClosed C
 #align category_theory.cartesian_closed CategoryTheory.CartesianClosed
 
+-- porting note: added to ease the port of `CategoryTheory.Closed.Types`
+/-- Constructor for `CartesianClosed C`. -/
+def CartesianClosed.mk (C : Type u) [Category.{v} C] [HasFiniteProducts C]
+    (h : ∀ X, IsLeftAdjoint (@MonoidalCategory.tensorLeft _ _
+      (monoidalOfHasFiniteProducts C) X)) :
+    CartesianClosed C :=
+  ⟨fun X => ⟨h X⟩⟩
+
 variable {C : Type u} [Category.{v} C] (A B : C) {X X' Y Y' Z : C}
 
 variable [HasFiniteProducts C] [Exponentiable A]

Mathlib/CategoryTheory/Closed/Types.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2020 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+
+! This file was ported from Lean 3 source module category_theory.closed.types
+! leanprover-community/mathlib commit 024a4231815538ac739f52d08dd20a55da0d6b23
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Limits.Presheaf
+import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
+import Mathlib.CategoryTheory.Limits.Shapes.Types
+import Mathlib.CategoryTheory.Closed.Cartesian
+
+/-!
+# Cartesian closure of Type
+
+Show that `Type u₁` is cartesian closed, and `C ⥤ Type u₁` is cartesian closed for `C` a small
+category in `Type u₁`.
+Note this implies that the category of presheaves on a small category `C` is cartesian closed.
+-/
+
+
+namespace CategoryTheory
+
+noncomputable section
+
+open Category Limits
+
+universe v₁ v₂ u₁ u₂
+
+variable {C : Type v₂} [Category.{v₁} C]
+
+section CartesianClosed
+
+instance (X : Type v₁) : IsLeftAdjoint (Types.binaryProductFunctor.obj X) where
+  right :=
+    { obj := fun Y => X ⟶ Y
+      map := fun f g => g ≫ f }
+  adj :=
+    Adjunction.mkOfUnitCounit
+      { unit := { app := fun Z (z : Z) x => ⟨x, z⟩ }
+        counit := { app := fun Z xf => xf.2 xf.1 } }
+
+instance : HasFiniteProducts (Type v₁) :=
+  hasFiniteProducts_of_hasProducts.{v₁} _
+
+instance : CartesianClosed (Type v₁) :=
+  CartesianClosed.mk _
+    (fun X => Adjunction.leftAdjointOfNatIso (Types.binaryProductIsoProd.app X))
+
+-- porting note: in mathlib3, the assertion was for `(C ⥤ Type u₁)`, but then Lean4 was
+-- confused with universes. It makes no harm to relax the universe assumptions here.
+instance {C : Type u₁} [Category.{v₁} C] : HasFiniteProducts (C ⥤ Type u₂) :=
+  hasFiniteProducts_of_hasProducts _
+
+instance {C : Type v₁} [SmallCategory C] : CartesianClosed (C ⥤ Type v₁) :=
+  CartesianClosed.mk _
+    (fun F =>
+      letI := FunctorCategory.prodPreservesColimits F
+      isLeftAdjointOfPreservesColimits (prod.functor.obj F))
+
+end CartesianClosed
+
+end
+
+end CategoryTheory