ここでtoTheseは同型

toThese :: (Maybe a, Maybe b) -> Maybe (These a b)

法則を使えばinclusion, subsetについて以下の等式が得られる。

inclusion . inclusion = inclusion
inclusion @X @X = id

subset <=< subset = subset
subset @X @X = Just

subset @X @y . include @y @X = Just

inclusion @(x∨y) @X . inclusion @X @(x ∧ y) = inclusion @(x∨y) @y . inclusion @y @(x ∧ y)