…es induced by chosen pullbacks (#31433)

We provide for a category `C` with chosen pullbacks, a cartesian monoidal structure on the slice categories `Over X` for all objects `X : C`. 

We also show that the functor `pullback f : Over X ⥤ Over Y` is naturally isomorphic to `toOver (Over.mk f): Over X ⥤ Over (Over.mk f)` post-composed with the iterated slice equivalence `Over (Over.mk f) ⥤ Over Y`.

This latter theorem will be crucial in relating closed objects in the slices to exponentiable morphisms in the base in `LocallyCartesianClosed.Basic.lean`

(Here `toOver` is defined to be the computable analogue of the functor `Over.star`.)

```mermaid
graph TD
  A[ChosenPullbackAlong.lean] --> A'[Over.lean] 
  A' --> B[Sections.lean]
  A --> C[ExponentiableMorphism.lean]
  B --> D[Basic.lean]
  C --> D
  D --> E[Types.lean]
  E --> F[Presheaves.lean]
  D --> G[Beck-Chevalley.lean]

  %% Define highlight style
  classDef highlight fill:#ffe599,stroke:#d4a017,stroke-width:2px;

  %% Apply to one node
  class A' highlight;
```

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

…es induced by chosen pullbacks (leanprover-community#31433)

We provide for a category `C` with chosen pullbacks, a cartesian monoidal structure on the slice categories `Over X` for all objects `X : C`. 

We also show that the functor `pullback f : Over X ⥤ Over Y` is naturally isomorphic to `toOver (Over.mk f): Over X ⥤ Over (Over.mk f)` post-composed with the iterated slice equivalence `Over (Over.mk f) ⥤ Over Y`.

This latter theorem will be crucial in relating closed objects in the slices to exponentiable morphisms in the base in `LocallyCartesianClosed.Basic.lean`

(Here `toOver` is defined to be the computable analogue of the functor `Over.star`.)

```mermaid
graph TD
  A[ChosenPullbackAlong.lean] --> A'[Over.lean] 
  A' --> B[Sections.lean]
  A --> C[ExponentiableMorphism.lean]
  B --> D[Basic.lean]
  C --> D
  D --> E[Types.lean]
  E --> F[Presheaves.lean]
  D --> G[Beck-Chevalley.lean]

  %% Define highlight style
  classDef highlight fill:#ffe599,stroke:#d4a017,stroke-width:2px;

  %% Apply to one node
  class A' highlight;
```

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

…es induced by chosen pullbacks (leanprover-community#31433)

We provide for a category `C` with chosen pullbacks, a cartesian monoidal structure on the slice categories `Over X` for all objects `X : C`. 

We also show that the functor `pullback f : Over X ⥤ Over Y` is naturally isomorphic to `toOver (Over.mk f): Over X ⥤ Over (Over.mk f)` post-composed with the iterated slice equivalence `Over (Over.mk f) ⥤ Over Y`.

This latter theorem will be crucial in relating closed objects in the slices to exponentiable morphisms in the base in `LocallyCartesianClosed.Basic.lean`

(Here `toOver` is defined to be the computable analogue of the functor `Over.star`.)

```mermaid
graph TD
  A[ChosenPullbackAlong.lean] --> A'[Over.lean] 
  A' --> B[Sections.lean]
  A --> C[ExponentiableMorphism.lean]
  B --> D[Basic.lean]
  C --> D
  D --> E[Types.lean]
  E --> F[Presheaves.lean]
  D --> G[Beck-Chevalley.lean]

  %% Define highlight style
  classDef highlight fill:#ffe599,stroke:#d4a017,stroke-width:2px;

  %% Apply to one node
  class A' highlight;
```

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>