Kerodon

Construction 5.2.0.1 (Covariant Transport for Left Covering Maps). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left covering map of simplicial sets. For each vertex $C \in \operatorname{\mathcal{C}}$, the fiber $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ is a discrete simplicial set, which we will identify with its underlying set of vertices (Remark 4.2.3.17). If $\widetilde{C}$ is a vertex of $\operatorname{\mathcal{E}}_{C}$ and $f: C \rightarrow D$ is an edge of $\operatorname{\mathcal{C}}$, then our assumption that $U$ is a left covering map guarantees that there is a unique edge $\widetilde{f}: \widetilde{C} \rightarrow f_{!}(\widetilde{C})$ of $\operatorname{\mathcal{E}}$ satisfying $U( \widetilde{f} ) = f$. The construction $\widetilde{C} \mapsto f_{!}(\widetilde{C})$ then determines a function $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$, which we will refer to as covariant transport along $f$.