Proposition [efr-002R]

Every vertical morphism f: x \to y in \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) has a companion, given by (I, x \cdot I \cong x \to y). A horizontal morphism (P, x \cdot P \to y) has a companion if and only if P \cong I.