ニョロニョロの確認

本編 随伴のニョロニョロ関係をTypeScriptで確認する - 檜山正幸のキマイラ飼育記 の手計算

• ε_P(X) P(η_X) = id_P(X)

まず定義：

A:Type;

η<X> :: X => A->X×A :=
  x:X => λa:A.(x, a);

ε<X> :: (A->X)×A => X :=
  (f, a):(A->X)×A => (f a);

ηとεはラムダ項じゃなくて射なので大きなラムダ式。=> は、射のプロファイル宣言でも射の記述でも使う。=>は大きなラムダΛの中置記法でもある。

  η<X>×A :: X×A => (A->X×A)×A
  ------------------- 定義
  (x:X => λa:A.(x, a))×A
  ------------------- 掛け算
  ((x, a'):X×A => (λa:A.(x, a), a'))

  ε<X×A> :: (A->X×A)×A => X×A
  ------------------- パラメータの置換
  (f, a):(A->X×A)×A => (f a)

セミコロンを文の終端に使ってしまったので、射の結合は|とする。

  η<X>×A | ε<X×A>
  ------------------- 定義
  ((x, a'):X×A => (λa:A.(x, a), a')) |  (f, a):(A->X×A)×A => (f a)
  -------------------  結合
  ((x, a'):X×A => (λa:A.(x, a), a'))
  -------------------  β変換
  ((x, a'):X×A => (x, a'))
  -------------------  カリー化
  ( =>λ(x, a'):X×A. (x, a'))