Sort u →
  {α : Type u_1} →
    {β : Type u_4} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          {u : β → α} →
            LowerAdjoint u →
              {α' : Type u_1} →
                {β' : Type u_4} →
                  [inst' : Preorder α'] → [inst'_1 : Preorder β'] → {u' : β' → α'} → LowerAdjoint u' → Sort u