English
Two left extensions α1: L.LeftExtension F1 and α2: L.LeftExtension F2 are universal in the same way if F1 ≅ F2 via e, and compatible e'. Then α1.IsUniversal ≃ α2.IsUniversal.
Русский
Два левых расширения α1 и α2 связаны изоморфизмом Ф1 ≅ Ф2 и совместимыми соответствиями e', то их универсальность эквивалентна: α1.IsUniversal ≃ α2.IsUniversal.
LaTeX
$$$\\alpha_1:\\,L.RightExtension?\\text{(устроено)}\\,\\alpha_2 \\Rightarrow \\alpha_1.IsUniversal \\equiv \\alpha_2.IsUniversal$$$
Lean4
/-- When two left extensions `α₁ : LeftExtension L F₁` and `α₂ : LeftExtension L F₂`
are essentially the same via an isomorphism of functors `F₁ ≅ F₂`,
then `α₁` is universal iff `α₂` is. -/
noncomputable def isUniversalEquivOfIso₂ (α₁ : LeftExtension L F₁) (α₂ : LeftExtension L F₂) (e : F₁ ≅ F₂)
(e' : α₁.right ≅ α₂.right) (h : α₁.hom ≫ whiskerLeft L e'.hom = e.hom ≫ α₂.hom) : α₁.IsUniversal ≃ α₂.IsUniversal :=
(IsInitial.isInitialIffObj (leftExtensionEquivalenceOfIso₂ L e).functor α₁).trans
(IsInitial.equivOfIso (StructuredArrow.isoMk e' (by simp [leftExtensionEquivalenceOfIso₂, h])))
