∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {L R : CategoryTheory.Functor C C} (adj : L ⊣ R)
  (α : R ⟶ CategoryTheory.Functor.id C) (c : C),
  ((CategoryTheory.conjugateEquiv adj CategoryTheory.Adjunction.id).symm α).app c =
    CategoryTheory.CategoryStruct.comp (adj.unit.app c) (α.app (L.obj c))