（Distributivity'1-'3より少し弱いバージョンで十分そうではある）

Distributivity'3は不要、なぜなら
undistrPairThese . distrPairThese = id
なので、'2から直ちに導かれるから。

Distributivity'2

distrPairThese <$> zip (align xs ys) zs ≡ align (zip xs zs) (zip ys zs)

これはxs, ysの要素だけ見たほうがよくて、

restrict :: forall a b. f a -> f b -> f a
restrict = zipWith const

を使って

restrict (align xs ys) zs ≡ align (restrict xs zs) (restrict ys zs)

Distributivity'1

align (zip xs ys) zs ≡ undistrThesePair <$> zip (align xs zs) (align ys zs)

これもxs, ysの要素だけ見ることができて、

expand :: forall a b. f a -> f b -> f (Maybe a)
expand as bs = justHere <$> align as bs

を使って

expand (zip xs ys) zs ≡ zipWith zip (expand xs zs) (expand ys zs)

Fを多項式Functorとする。

F a = Σ_{x ∈ M} (E x -> a)

F aの要素は(x :: M, f :: E x -> a)と書く。

FがZip (+Align)でもあるとき、それらの法則から

- Mは(Bounded) Distributive Lattice (0,1,∨,∧,≤)
- E(0) ~ Void

であって、2つの関数

inclusion :: (x ≤ y) => E x -> E y
subset :: (x ≤ y) => E y -> Maybe (E x)

から

zip (x,f) (y,g) = (x ∧ y, \i -> (f (inclusion i), g (inclusion i)))
Just <$> align (x,f) (y,g) = (x ∨ y, \i -> toThese (f <$> subset i, g <$> subset i))

とzip, alignが定義される

ここで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)