¶Intersection of s₁ ≤ and ≁ t₂
The intersection of a lower bound and an incomparible depends on how the two types are related.
(s₁ ≤) ∧ (≁ t₂) = ∅ if t₂ ⊆ s₁
= (s₁ ≤) ∧ (≁ t₂) otherwise
¶Equationally
⟦s₁ ≤⟧ = {x | x ⊆ t₁}
⟦≁ t₂⟧ = {x | x ⊈ t₂ ∧ t₂ ⊈ x}
If t₂ ⊆ s₁, the key step is that s₁ ⊆ x implies t₂ ⊆ x by transitivity, which contradicts the incomparible constraint on t₂.
⟦(s₁ ≤) ∧ (≁ t₂)⟧
= {x | s₁ ⊆ x} ∩ {x | x ⊈ t₂ ∧ t₂ ⊈ x}
= {x | s₁ ⊆ x ∧ x ⊈ t₂ ∧ t₂ ⊈ x}
= {x | s₁ ⊆ x ∧ t₂ ⊆ x ∧ x ⊈ t₂ ∧ t₂ ⊈ x}
= {x | s₁ ⊆ x ∧ false ∧ x ⊈ t₂}
= {x | false}
= ∅
Otherwise, the two constraints cannot be simplified.