diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr
index 856c4ea..0db17b5 100644
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@@ -81,15 +81,12 @@ compat pi Any = True
 compat pi rh  = pi == rh
 
 
-||| "π ∧ ρ"
+||| "π ∨ ρ"
 |||
 ||| returns some quantity τ where π ≤ τ and ρ ≤ τ, if one exists.
 public export
 lub : Qty -> Qty -> Maybe Qty
-lub p q =
-  if p == Any || q == Any then Just Any
-  else if p == q then Just p
-  else Nothing
+lub p q = Just $ if p == q then p else Any
 
 
 ||| to maintain subject reduction, only 0 or 1 can occur