証明.

省略する。

証明.

条件 1 ⇒ 条件 2:まず、 flat : (A⇀[B,C])⇀[A×B,C] ≡ λm.first(arrm)⋙app とおく。 これが条件 2 にある 2 つの等式を満たすことを示す。

1 つ目の等式を示す。 まず、 flat(sharpH) = first(arr(λa.arr(λb.⟨a,b⟩)⋙H))⋙app♡1 である。 ここで、 λa.arr(λb.⟨a,b⟩)⋙H = (λa.arr(λb.⟨a,b⟩))⊳(λf.f⋙H) であるから、 first(arr(λa.arr(λb.⟨a,b⟩)⋙H))⋙app = first(arr(λa.arr(λb.⟨a,b⟩))⋙first(arr(λf.f⋙H))⋙app = first(arr(λa.arr(λb.⟨a,b⟩))⋙app⋙H = arrid⋙H = H♡2 が成り立つ。 式 ♡1,♡2 を合わせれば、 導きたかった式が得られる。

2 つ目の等式を示す。 まず、 sharp(flatM) = λa.arr(λb.⟨a,b⟩)⋙first(arrM)⋙app = λa.arr(λb.⟨a,b⟩)⋙arr(M×id)⋙app = λa.arr((λb.⟨a,b⟩)⊳(M×id))⋙app = λa.arr(λb.⟨Ma,b⟩)⋙app♤1 が成り立つ。 さて、 lu≡λb󰎘.⟨⋆,b󰎘⟩ とおくと、 lu と snd は互いに逆関数になっているから、 λb.⟨Ma,b⟩ = λb.⟨arrlu⋙arrsnd⋙Ma,b⟩ = (λb.⟨arrlu,b⟩)⊳((λf.f⋙arrsnd⋙Ma)×id) が成り立つ。 したがって、 G≡arrsnd⋙Ma とおけば、 λa.arr(λb.⟨Ma,b⟩)⋙app = λa.arr(λb.⟨arrlu,b⟩)⋙arr((λf.f⋙G)×id)⋙app = λa.arr(λb.⟨arrlu,b⟩)⋙first(arr(λf.f⋙G))⋙app = λa.arr(λb.⟨arrlu,b⟩)⋙app⋙G♤2 が成り立つ。 さらに、 λb.⟨arrlu,b⟩ = lu⊳snd⊳(λb.⟨arrlu,b⟩) = lu⊳((λu.arrlu)×id) = lu⊳((λu.arr(λb󰎘.⟨⋆,b󰎘⟩))×id) = lu⊳((λu.arr(λb󰎘.⟨u,b󰎘⟩))×id) であるから、 λa.arr(λb.⟨arrlu,b⟩)⋙app⋙G = λa.arrlu⋙arr((λu.arr(λb󰎘.⟨u,b󰎘⟩))×id)⋙app⋙G = λa.arrlu⋙first(arr(λu.arr(λb󰎘.⟨u,b󰎘⟩))⋙app⋙G = λa.arrlu⋙arrid⋙G = λa.arrlu⋙G = λa.arrlu⋙arrsnd⋙Ma = λa.Ma = M♤3 である。 式 ♤1,♤2,♤3 を合わせれば、 導きたかった式が得られる。

条件 2 ⇒ 条件 1:この場合は、 app : [[A,B]×A,B] ≡ flatid とおけば良い。 これが条件 1 にある 3 つの等式を満たすことを示す。 仮定により sharp は逆関数をもつから、 示したい等式の両辺に sharp を適用した等式を示せば良い。

1 つ目の等式を示す。 左辺に sharp を適用したものは、 sharp(first(arr(λa.arr(λb.⟨a,b⟩)))⋙app) = (λa.arr(λb.⟨a,b⟩))⊳sharpapp = (λa.arr(λb.⟨a,b⟩))⊳sharp(flatid) = λa.arr(λb.⟨a,b⟩) と計算できる。 また、 右辺に sharp を適用したものは、 sharp(arrid) = λa.arr(λb.⟨a,b⟩)⋙arrid = λa.arr(λb.⟨a,b⟩) と計算できる。 両者は一致しているので、 これで示された。

2 つ目の等式を示す。 左辺に sharp を適用したものは、 sharp(first(arr(λg.F⋙g))⋙app) = (λg.F⋙g)⊳sharpapp = (λg.F⋙g)⊳sharp(flatid) = λg.F⋙g と計算できる。 また、 右辺に sharp を適用したものは、 sharp(secondF⋙app) = λg.F⋙sharpappg = λg.F⋙sharp(flatid)g = λg.F⋙g と計算できる。 両者は一致しているので、 これで示された。

3 つ目の等式も全く同様に示すことができる。

証明.

定理 4.3 と命題 5.3 から従う。