English
Suppose φ is strongly cocartesian with respect to p and f. If φ' : a → b' and ψ : b → b' are such that g ≫ ψ = φ', and if ψ and map p f φ hf' φ' are both morphisms from b to b' lifting φ' through g, then ψ equals map p f φ hf' φ'. This expresses the uniqueness of the induced map given the universal property.
Русский
Пусть φ является сильно когартезианальным относительно p и f. Если φ' : a → b' и ψ : b → b' таковы, что g ∘ ψ = φ', и если ψ и map p f φ hf' φ' являются подъемами φ' по g, тогда ψ = map p f φ hf' φ'.
LaTeX
$$$\psi = \mathrm{map}\ p\ f\ \phi\ hf'\ \phi'$$$
Lean4
/-- Given a diagram
```
a --φ--> b b'
| | |
v v v
R --f--> S --g--> S'
```
such that `φ` is strongly co-Cartesian, and morphisms `φ' : a ⟶ b'`, `ψ : b ⟶ b'` such that
`g ≫ ψ = φ'`. Then `ψ` is the map induced by the universal property. -/
theorem map_uniq (ψ : b ⟶ b') [IsHomLift p g ψ] (hψ : φ ≫ ψ = φ') : ψ = map p f φ hf' φ' :=
(Classical.choose_spec <| universal_property p f φ _ _ hf' φ').2 ψ ⟨inferInstance, hψ⟩
