Kerodon

Remark 7.4.5.12. In the statement of Theorem 7.4.5.11, the covariant refraction diagram $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ and the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{QC}}^{< \lambda }$ are only well-defined up to isomorphism (as objects of the $\infty $-categories $\operatorname{Fun}( \operatorname{\mathcal{E}}, \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} })$ and $\operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleright }, \operatorname{\mathcal{QC}}^{< \lambda } )$, respectively). However, the hypothesis and conclusion of the theorem depend only on their isomorphism classes (see Exercise 6.3.1.11 and Corollary 7.1.3.14).