Lean4
/-- If the left extension defined by `α : F₀ ⟶ L ⋙ F₁` is universal,
then for every `L' : D ⥤ D'`, `F₁ : D ⥤ H`, if an extension
`b : L'.LeftExtension F₁` is such that the "pasted" extension
`(LeftExtension.precomp₂ L' α).obj b` is universal, then `b` is itself
universal. -/
def isUniversalOfPrecomp₂ (hα : (LeftExtension.mk F₁ α).IsUniversal) {b : L'.LeftExtension F₁}
(hb : ((LeftExtension.precomp₂ L' α).obj b).IsUniversal) : b.IsUniversal :=
by
letI (y : L'.LeftExtension F₁) : Unique (b ⟶ y) :=
by
let u : (LeftExtension.precomp₂ L' α).obj b ⟶ (LeftExtension.precomp₂ L' α).obj y := hb.to _
haveI := u.w
simp only [precomp₂_obj_left, const_obj_obj, precomp₂_obj_right, whiskeringLeft_obj_obj, StructuredArrow.left_eq_id,
const_obj_map, id_comp, whiskeringLeft_obj_map] at this
refine
⟨⟨StructuredArrow.homMk u.right <| by
apply hα.hom_ext
ext t
have := congr_app u.w t
simp only [precomp₂_obj_left, const_obj_obj, precomp₂_obj_right, whiskeringLeft_obj_obj, comp_obj,
StructuredArrow.left_eq_id, const_obj_map, id_comp, precomp₂_obj_hom_app, whiskeringLeft_obj_map,
NatTrans.comp_app, whiskerLeft_app, assoc] at this
simp [this]⟩,
fun a => ?_⟩
dsimp
ext1
apply hb.hom_ext
ext t
have := congr_app u.w t
have a_w := a.w
simp only [precomp₂_obj_left, const_obj_obj, precomp₂_obj_right, whiskeringLeft_obj_obj, comp_obj,
StructuredArrow.left_eq_id, const_obj_map, id_comp, precomp₂_obj_hom_app, whiskeringLeft_obj_map,
NatTrans.comp_app, whiskerLeft_app, assoc] at this a_w
simp [← this, a_w]
apply IsInitial.ofUnique
