モノイド閉圏の事例: ベータ変換等式

  • X,A,Y(f)□A^);ev = f  \newcommand{\For}{\mbox{For}\:\:}\newcommand{\cat}[1]{{\mathcal {#1}}} \newcommand{\id}{\mbox{id}}

\For f : X\otimes A \to Y \:\mbox{in}\: \cat{C},\\ (\Lambda^{X,A}_Y(f)\otimes \id_A);{^A ev_X} = f

ΦX,A,Y(f) = Φ(f) = F と置いて、(ΦX,A,Y(f)□A^) = F□A^ を計算する。

F□A^ : X□A→hom(A, Y)□A
=
[
  λ0(x, a)∈A□A.(
     (F(x), a) ∈hom(A, Y)□A
  )
  ALSO
  λ1(x→x', a)∈A□A.(
     (F(x→x'), a) ∈hom(A, Y)□A
  )
  OR
  λ1(x, a→a')∈A□A.(
     (F(x), a→a') ∈hom(A, Y)□A
  )
] : X□A→hom(A, Y)□A
=
λ[(x, a) ALSO (x→x', a) OR (x, a→a')∈X□A.(
  [
   ( (F(x), a) ∈hom(A, Y)□A)
   ALSO
   ( (F(x→x'), a) ∈hom(A, Y)□A)
   OR
   ( (F(x), a→a') ∈hom(A, Y)□A)
  ] ∈hom(A, Y)□A
)

これに ev〈エバル | 評価射〉を後結合すると、

λ[(x, a) ALSO (x→x', a) OR (x, a→a')∈X□A.(
  [
   ( F(x)(a) ∈Y)
   ALSO
   ( (F(x→x')(a) ∈Y)
   OR
   ( (F(x)(a→a') ∈Y)
  ] ∈Y
)

という写像になる。F = Φ(f) だったので、これは f に他ならない。したがって、

  • X,A,Y(f)□A^);ev = f

が成立する。