Lean4
/-- A left Kan lift of the identity along `u` such that `u` commutes with is a left adjoint
to `u`. The unit of this adjoint is given by the unit of the Kan lift. -/
def adjunction {u : b ⟶ a} {t : LeftLift u (𝟙 a)} (H : IsKan t) (H' : IsKan (t.whisker u)) : t.lift ⊣ u :=
let ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc <| .mk _ <| (ρ_ u).hom ≫ (λ_ u).inv
have Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv := by
simpa [rightZigzag, bicategoricalComp] using H'.fac <| .mk _ <| (ρ_ u).hom ≫ (λ_ u).inv
{ unit := t.unit
counit := ε
left_triangle := by
apply (cancel_epi (λ_ _).inv).mp
apply H.hom_ext
calc
_
_ = 𝟙 _ ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 _ := by bicategory
_ = 𝟙 _ ⊗≫ (_ ◁ t.unit ≫ t.unit ▷ _) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 _ := by rw [leftZigzag]; bicategory
_ = 𝟙 _ ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 _ := by rw [whisker_exchange]; bicategory
_ = _ := by rw [← rightZigzag, Hε]; bicategory
right_triangle := Hε }
