Sort u →
  {α : Type u_8} →
    {β : Type u_9} →
      [inst : CompleteLattice α] →
        [inst_1 : CompleteLattice β] →
          CompleteLatticeHom α β →
            {α' : Type u_8} →
              {β' : Type u_9} →
                [inst' : CompleteLattice α'] → [inst'_1 : CompleteLattice β'] → CompleteLatticeHom α' β' → Sort u