モノイド閉圏の事例： カリー化の自然性 (続き2)

前の記事の続き。後でひとつの記事にまとめるかも。

真っすぐなスライディング

• Φ_X,A,Y'( f;q ) = Φ_X,A,Y(f);hom(A, q) : X→hom(A,Y')

左辺：

Φ( f;q )  : X→hom(A,Y')
=
[
  λ0x∈X.(
    [
      λ0a∈A.( q(f(x, a)) ∈Y')
      ALSO
      λ1a→a'∈A.( q(f(x, a→a')) ∈Y')
    ]  ∈Hom(X, Y')
   )
   ALSO
   λx→x'∈X.(
     [
       λ01a∈A.( q(f(x→x', a)) ∈Y')
     ] ∈Defm(A, Y')
    )
] ∈Hom(X, hom(A, Y'))
=
λ{x ALSO x→x'}∈X.(
 {
    [
      λ0a∈A.( q(f(x, a)) ∈Y')
      ALSO
      λ1a→a'∈A.( q(f(x, a→a')) ∈Y')
    ]  ∈Hom(X, Y')
    ALSO
    [
      λ01a∈A.( q(f(x→x', a)) ∈Y')
    ] ∈Defm(A, Y')
 }
)

準備：

Φ(f) : X→hom(A, Y)
=
[
  λ0x∈X.(
    [
      λ0a∈A.( f(x, a) ∈Y)
      ALSO
      λ1a→a'∈A.( f(x, a→a') ∈Y)
    ]  ∈Hom(A, Y)
   )
   ALSO
   λx→x'∈X.(
     [
       λ01a∈A.( f(x→x', a) ∈Y)
     ] ∈Defm(A, Y)
    )
] ∈Hom(X, hom(A, Y))
=
λ{x ALSO x→x'}∈X.(
 {
   [
     λ0a∈A.( f(x, a) ∈Y)
     ALSO
     λ1a→a'∈A.( f(x, a→a') ∈Y)
   ]  ∈Hom(X, Y)
   ALSO
   [
     λ01a∈A.( f(x→x', a) ∈Y)
   ] ∈Defm(A, Y)
 } ∈Hom(X, hom(A, Y))
)


hom(A, q:Y→Y') :hom(A, Y)→hom(A, Y')
=
[
  λ0u∈hom(A, Y).( u;q ∈Hom(A, Y) )
  ALSO
  λ1u⇒v∈hom(A, Y).( (u⇒v);;q  ∈Defm(A, Y) )
]
=
λ{u ALSO u⇒v}∈hom(A, Y).(
 {
   ( u;q ∈Hom(A, Y))
    ALSO
   ( (u⇒v);;q ∈Defm(A, Y))
 }
)


右辺  : X→hom(A,Y')
=
Φ(f);hom(A, q)
=
λ{x ALSO x→x'}∈X./(
 {
   ( u;q ∈Hom(A, Y'))
    ALSO
   ( (u⇒v);;q ∈Defm(A, Y'))
  }
  /
  {u ALSO u⇒v} = Φ(f)({x ALSO x→x'})
)/
=
λ{x ALSO x→x'}∈X.(
 {
   ( Φ(f)(x);q ∈Hom(A, Y'))
    ALSO
   ( (Φ(f)(x)⇒Φ(x)(v));;q ∈Defm(A, Y'))
  }
)

左辺と右辺を比べてみる：

左辺 : X→hom(A,Y') =
λ{x ALSO x→x'}∈X.(
 {
    [
      λ0a∈A.( q(f(x, a)) ∈Y')
      ALSO
      λ1a→a'∈A.( q(f(x, a→a')) ∈Y')
    ]  ∈Hom(A, Y')
    ALSO
    [
      λ01a∈A.( q(f(x→x', a)) ∈Y')
    ] ∈Defm(A, Y')
 }
)

右辺 : X→hom(A,Y') =
λ{x ALSO x→x'}∈X.(
 {
   ( Φ(f)(x);q ∈Hom(A, Y'))
    ALSO
   ( (Φ(f)(x)⇒Φ(x)(v));;q ∈Defm(A, Y'))
  }
)

等式を示すには、次をターゲット（証明の目標）にすればよい。

[
   λ0a∈A.( q(f(x, a)) ∈Y')
   ALSO
   λ1a→a'∈A.( q(f(x, a→a')) ∈Y')
]  ∈Hom(A, Y')
=
( Φ(f)(x);q ∈Hom(A, Y'))


[
 λ01a∈A.( q(f(x→x', a)) ∈Y')
] ∈Defm(A, Y')
=
( (Φ(f)(x)⇒Φ(x)(v));;q ∈Defm(A, Y'))

この2つの等式は、Φ〈カリー化〉の定義／;〈写像の結合〉の定義／;;〈変形と写像の結合〉の定義から出るので、計算は割愛する。