English
Let p be a functor that is strongly cocartesian with respect to a morphism f: R → S and φ: a → b. For any g: S → S', any f': R → S' with f' = f ∘ g, and any φ': a → b', there is a canonical lift map map p f φ hf' φ' such that φ ≫ map p f φ hf' φ' = φ'. This expresses the universal property of the lift: composing φ with the induced lift gives φ'.
Русский
Пусть p является функционором, над которым φ является сильно когартезианальной по отношению к морфизму f: R → S и φ: a → b. Для любой g: S → S', для любого f': R → S' с условием f' = f ∘ g и для φ': a → b' существует каноническое отображение map p f φ hf' φ', такое что φ ∘ map p f φ hf' φ' = φ'. Это выражает универсальное свойство подъема: композиция φ с индуцированным подъемом даёт φ'.
LaTeX
$$$\phi \;\circ\; \mathrm{map}\ (p,f,\phi,hf',\phi')\ =\ \phi'$$$
Lean4
@[reassoc (attr := simp)]
theorem fac : φ ≫ (map p f φ hf' φ') = φ' :=
(Classical.choose_spec <| universal_property p f φ _ _ hf' φ').1.2
