∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.CostructuredArrow.isoMk
          (CategoryTheory.Iso.refl
            (((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.comp
                    (CategoryTheory.CategoryOfElements.toCostructuredArrow F)).obj
                X).left)
          ⋯)
      ⋯