Union (|) and intersection (&) types, introduced in Scala 3 (but also available in e.g. TypeScript and Flow) enable expressive type-level programming and can simulate many natural programming constructs. On the other hand, their practical deployments have faced several challenges: inefficient subtype checking, incomplete reasoning with type bounds and even unsoundness. To solve these problems, we propose orthologic-based subtyping. Concretely, types are interpreted in a free ortholattice extended with monotonic and antimonotonic function symbols. This yields an O(𝑛2 (1+𝑚)) subtyping algorithm (where 𝑚 is the number of subtyping assumptions) and an O(𝑛2) normalization procedure that always produces the smallest equivalent type. Ortholattices are a weakening of Boolean algebras that do not necessarily satisfy the distributivity law. In particular, they are a sound approximation of the set-theoretic model of union and intersection types. This framework naturally supports covariant and contravariant type constructors, record types, nominal subtyping with classes and traits, constrained polymorphism, and negation types—offering a principled, efficient, and sound foundation for union and intersection types.