$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 5.2.7.2. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left covering map of simplicial sets, and let $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \operatorname{Set}$ be the homotopy transport representation of Proposition 5.2.0.3. Then there is a canonical isomorphism of simplicial sets
\[ \operatorname{\mathcal{E}}\simeq \operatorname{\mathcal{C}}\times _{ \operatorname{N}_{\bullet }( \mathrm{h} \mathit{\operatorname{\mathcal{C}}} )} \operatorname{N}_{\bullet }( \int _{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}} \operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}). \]
Proof.
Every vertex $X \in \operatorname{\mathcal{E}}$ can be regarded as an element of the set $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( U(X) )$, and the construction $(X \in \operatorname{\mathcal{E}}) \mapsto ( \operatorname{\mathcal{E}}_{U(X)}, X)$ determines a functor $\widetilde{\operatorname{hTr}}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{E}}} \rightarrow \operatorname{Set}_{\ast }$. Let us identify $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ with a morphism of simplicial sets from $\operatorname{\mathcal{C}}$ to $\operatorname{N}_{\bullet }(\operatorname{Set})$ and $\widetilde{\operatorname{hTr}}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ with a morphism of simplicial sets from $\operatorname{\mathcal{E}}$ to $\operatorname{N}_{\bullet }(\operatorname{Set}_{\ast } )$, so that we have a commutative diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r]^-{ \widetilde{\operatorname{hTr}}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} } & \operatorname{N}_{\bullet }( \operatorname{Set}_{\ast } ) \ar [d] \\ \operatorname{\mathcal{C}}\ar [r]^-{ \operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} } & \operatorname{N}_{\bullet }( \operatorname{Set}) } \]
which we can identify with a morphism of simplicial sets $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{N}_{\bullet }( \mathrm{h} \mathit{\operatorname{\mathcal{C}}}) } \operatorname{N}_{\bullet }( \int _{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}} \operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}})$. Since $U$ and the projection map $\int _{\operatorname{\mathcal{C}}} \operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ are both left covering maps (Remark 5.2.6.9), it follows that $V$ is a left covering map (Remark 4.2.3.14). By construction, $V$ is bijective at the level of vertices, and is therefore an isomorphism of simplicial sets (Proposition 4.2.3.19).
$\square$