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

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

カーブに沿ったスライディング

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

左辺のΦの内側：

(X^□p);f : X□A'→Y =
[
 λ(x, a')∈X□A'.( f(x, p(a')) ∈Y)
 ALSO
 λ(x→x', a')∈X□A'.( f(x→x', p(a')) ∈Y)
 OR
 λ(x, a'→a'')∈X□A'.( f(x, p(a'→a'')) ∈Y)
] : X□A'→Y

左辺：

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

右辺を計算するにあたって、Φ(f) = F とする。

• F : X→hom(A, Y)
• p:A→A'
• hom(p, Y) : hom(A, Y)→hom(A', Y)

右辺：

F;hom(p, Y)
= F;(λτ∈hom(A, Y).( hom(p, Y)(τ) ))
=
λξ∈X./( hom(p, Y)(τ) / τ = F(ξ) )/
=
λ{x ALSO x→x'}∈X./(
  hom(p, Y)({u ALSO u⇒v})
  /
  {u ALSO u⇒v} = F({x ALSO x→x'})
)/
=
λ{x ALSO x→x'}∈X./(
  [
    λ0u∈hom(A, Y).( p;u ∈Hom(A, Y) )
    ALSO
    λ1u⇒v∈hom(A, Y).( p;;(u⇒v) ∈Defm(A, Y) )
  ]({u ALSO u⇒v})
  /
  {u ALSO u⇒v} = F({x ALSO x→x'})
)/
=
λ{x ALSO x→x'}∈X./(
  {
    ( p;u ∈Hom(A, Y) )
    ALSO
    ( p;;(u⇒v) ∈Defm(A, Y) )
  }
  /
  {u ALSO u⇒v} = F({x ALSO x→x'})
)/
=
λ{x ALSO x→x'}∈X.(
  {
    ( p;F(x) ∈Hom(A, Y) )
    ALSO
    ( p;;(F(x→x')) ∈Defm(A, Y) )
  }
)
=
[
  λ0x∈X.( p;F(x) ∈Hom(A, Y) )
  ALSO
  λ1x→x'∈X.( p;;(F(x→x')) ∈Defm(A, Y) )
]

ここで、次を計算する。

• For x∈X₍₀₎, p;F(x) ∈Hom(A, Y)

F(x)
=
 [
   λ0a∈A.( f(x, a) ∈Y)
    ALSO
   λ1t→t'∈A.( f(x, t→t') ∈Y) /* 都合により t→t' */
 ]  ∈Hom(A, Y)



p;F(x)
= p;(λξ∈A.( F(x)(ξ) )
= λτ∈A'./( F(x)(ξ) / ξ = p(τ) )/
=
λ{a' ALSO a'→a''}∈A'./(
  F(x)({{a ALSO t→t'}})
  / {a ALSO t→t'} = p({a' ALSO a'→a''})
)/
=
λ{a' ALSO a'→a''}∈A'./(
 [
   λ0a∈A.( f(x, a) ∈Y)
    ALSO
   λ1t→t'∈A.( f(x, t→t') ∈Y) /* 都合により t→t' */
 ]({{a ALSO t→t'}})
  / {a ALSO t→t'} = p({a' ALSO a'→a''})
)/
=
λ{a' ALSO a'→a''}∈A'./(
 {
   ( f(x, a) ∈Y)
    ALSO
   ( f(x, t→t') ∈Y)
 }
  / {a ALSO t→t'} = p({a' ALSO a'→a''})
)/
=
λ{a' ALSO a'→a''}∈A'.(
 {
   ( f(x, p(a')) ∈Y)
   ALSO
   ( f(x, p(a'→a'')) ∈Y)
 }
)
=
[
 λ0a'∈A'.( f(x, p(a')) ∈Y)
 ALSO
 λ1a'→a''∈A'.( f(x, p(a'→a'')) ∈Y)
]

さらに次を計算する。

• For x→x'∈X₍₁₎, p;;(F(x→x')) ∈Defm(A, Y)

F(x→x')
=
λ01a∈A.( f(x→x' a) ∈Y)


p;;F(x→x')
=
p;;(λ01a∈A.( f(x→x' a) ∈Y))
=
λ01a'∈A'./(
  ( f(x→x' a) ∈Y)
  /
  a = p(a')
)/
=
λ01a'∈A'./(
  ( f(x→x' a) ∈Y)
  /
  a = p(a')
)/
=
λ01∈A'.( f(x→x' p(a')) ∈Y)

以上の計算を組み合わせれば、左辺＝右辺が出る。

次の記事に続く。