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)

... これらの等式はE xがそれぞれE 1のある部分集合と見做せて、inclusionがその部分集合の包含写像と見做せると言える。

これがZip/Align則の"想定している"振る舞いなので、Zip/Align則はこれで完全であると言っても良い！

では余剰な法則は無いのか？
Zip単独、Align単独の法則は余剰なものは無いだろう。

Absorption lawを入れるならばべき等律は省けるかもしれない（が、Zip/Align単独でも使えるようにしたいため、省略はしないでよいだろう）

Distributivityは、束論としてはどちらか片方のみでよいはずだが…

Distributivityは(2)から(1)が導ける、OK!