English
If α1: RightExtension L F1 and α2: RightExtension L F2 are related by e: F1 ≅ F2 and e': α1.left ≅ α2.left with a compatibility condition, then α1.IsUniversal ≃ α2.IsUniversal.
Русский
Если два правых расширения α1 и α2 связаны изоморфизмом F1 ≅ F2 и соответствием e': α1.left ≅ α2.left с совместимостью, то их универсальность эквивалентна.
LaTeX
$$$\\alpha_1.IsUniversal \\simeq \\alpha_2.IsUniversal$$$
Lean4
/-- When two right extensions `α₁ : RightExtension L F₁` and `α₂ : RightExtension L F₂`
are essentially the same via an isomorphism of functors `F₁ ≅ F₂`,
then `α₁` is universal iff `α₂` is. -/
noncomputable def isUniversalEquivOfIso₂ (α₁ : RightExtension L F₁) (α₂ : RightExtension L F₂) (e : F₁ ≅ F₂)
(e' : α₁.left ≅ α₂.left) (h : whiskerLeft L e'.hom ≫ α₂.hom = α₁.hom ≫ e.hom) : α₁.IsUniversal ≃ α₂.IsUniversal :=
(IsTerminal.isTerminalIffObj (rightExtensionEquivalenceOfIso₂ L e).functor α₁).trans
(IsTerminal.equivOfIso (CostructuredArrow.isoMk e' (by simp [rightExtensionEquivalenceOfIso₂, h])))
