English
If two lifts ψ, ψ' of a base via g satisfy ψ ≫ φ = ψ' ≫ φ, then ψ = ψ'.
Русский
Если два подъёма ψ, ψ' по основанию через g удовлетворяют ψ ≫ φ = ψ' ≫ φ, тогда ψ = ψ'.
LaTeX
$$$\\forall ψ, ψ' : a' \\to a\\; [IsHomLift(p,g,ψ)]\\,[IsHomLift(p,g,ψ')]\\ (ψ \\circ φ = ψ' \\circ φ) \\Rightarrow ψ = ψ'$$$
Lean4
/-- Given two commutative squares
```
a --φ--> b --ψ--> c
| | |
v v v
R --f--> S --g--> T
```
such that `φ ≫ ψ` and `ψ` are strongly Cartesian, then so is `φ`. -/
protected theorem of_comp [IsStronglyCartesian p g ψ] [IsStronglyCartesian p (f ≫ g) (φ ≫ ψ)] [IsHomLift p f φ] :
IsStronglyCartesian p f φ where
universal_property' := by
intro a' h τ hτ
have h₁ : IsHomLift p (h ≫ f ≫ g) (τ ≫ ψ) := by simpa using IsHomLift.comp p (h ≫ f) _ τ ψ
use map p (f ≫ g) (φ ≫ ψ) (f' := h ≫ f ≫ g) rfl (τ ≫ ψ)
refine
⟨⟨inferInstance, ?_⟩, ?_⟩
/- The fact that `π ≫ φ = τ` follows from `π ≫ φ ≫ ψ = τ ≫ ψ` and the universal property of
`ψ`. -/
·
apply
IsStronglyCartesian.ext p g ψ (h ≫ f)
(by simp)
-- Finally, the uniqueness of `π` comes from the universal property of `φ ≫ ψ`.
· intro π' ⟨hπ'₁, hπ'₂⟩
apply map_uniq
simp [hπ'₂.symm]
