Kerodon

Corollary 4.4.5.10. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $\operatorname{Isom}(\operatorname{\mathcal{C}}) \subseteq \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$ be the full subcategory spanned by the isomorphisms, and let $\operatorname{ev}_{0},\operatorname{ev}_1: \operatorname{Isom}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the functors given by evaluation at the vertices $0,1 \in \Delta ^1$. Then the functors $\operatorname{ev}_{0}$ and $\operatorname{ev}_{1}$ are trivial Kan fibrations.