{F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : MulZeroOneClass α] →
            [inst_3 : MulZeroOneClass β] →
              [inst_4 : FunLike F α β] → [OrderHomClass F α β] → [MonoidWithZeroHomClass F α β] → CoeTC F (α →*₀o β)