English
If two lifts ψ, ψ' from b to b' over the same base morphism g: S → S' satisfy φ ≫ ψ = φ ≫ ψ', then ψ = ψ'. This extensionality follows from the uniqueness part of the universal property.
Русский
Если два подъема ψ, ψ' из b в b' над одинаковым основанием g: S → S' удовлетворяют φ ≫ ψ = φ ≫ ψ', тогда ψ = ψ'. Это следствие уникальности свойства универсума.
LaTeX
$$$\text{If } φ \;\gg\; ψ = φ \;\gg\; ψ' \text{ then } ψ = ψ'$$$
Lean4
/-- Given a diagram
```
a --φ--> b b'
| | |
v v v
R --f--> S --g--> S'
```
such that `φ` is strongly co-Cartesian, and morphisms `ψ ψ' : b ⟶ b'` such that
`g ≫ ψ = φ' = g ≫ ψ'`. Then we have that `ψ = ψ'`. -/
protected theorem ext (φ : a ⟶ b) [IsStronglyCocartesian p f φ] {S' : 𝒮} {b' : 𝒳} (g : S ⟶ S') {ψ ψ' : b ⟶ b'}
[IsHomLift p g ψ] [IsHomLift p g ψ'] (h : φ ≫ ψ = φ ≫ ψ') : ψ = ψ' := by
rw [map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ rfl, map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ' h.symm]
