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