We define an exponentiable morphism `f : I ⟶ J` to be a morphism with a chosen pullback functor
`Over J ⥤ Over I` together with a right adjoint, called the pushforward functor.

We use this PR in the PR branch `lccc-basic`.  

```mermaid
graph TD
  A[ChosenPullbacksAlong.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 C highlight;
```

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

…1332)

We define an exponentiable morphism `f : I ⟶ J` to be a morphism with a chosen pullback functor
`Over J ⥤ Over I` together with a right adjoint, called the pushforward functor.

We use this PR in the PR branch `lccc-basic`.  

```mermaid
graph TD
  A[ChosenPullbacksAlong.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 C highlight;
```

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

…1332)

We define an exponentiable morphism `f : I ⟶ J` to be a morphism with a chosen pullback functor
`Over J ⥤ Over I` together with a right adjoint, called the pushforward functor.

We use this PR in the PR branch `lccc-basic`.  

```mermaid
graph TD
  A[ChosenPullbacksAlong.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 C highlight;
```

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>