1: \begin{definition}

2: Let $p_1 \colon E_1 \to B$, $p_2 \colon E_2 \to B$ be fibrations over a common base (as in Definition~\ref{def:internal-eq}).

3: 

4: Define $\extHomLHInv_B(E_1,E_2)$ to be the set of \emph{maps with a left homotopy inverse} from $X$ to $Y$, i.e.\ triples $(f,g,H)$, where $f \colon E_1 \to E_2$ and $g \colon E_2 \to E_1$ are maps over $B$, and $H$ is a fibred homotopy from $g \cdot f$ to $1_{E_1}$, defined using the fibred path space $\paths_B(E_1)$ (as used for the $\IdStrux$-structure in the proof of Theorem~\ref{thm:the-model-in-ssets}).

5: 

6: Similarly, define $\extHomRHInv_B(E_1,E_2)$ to consist of triples $(f,g,H)$, where $f, g$ are as before, and $H$ is now a fibred homotopy from $f \cdot g$ to $1_{E_2}$, defined using $\paths_B(E_2)$.

7: 

8: Finally, these both come with evident projections to $\Hom_B(E_1,E_2)$; define $\extHIso_B(E_1,E_2) := \extHomLHInv_B(E_1,E_2) \times_{\Hom_B(E_1,E_2)} \extHomRHInv_B(E_1,E_2).$

9: \end{definition}

10: