Leanの論理再考 2

Leanの論理再考 - (新) 檜山正幸のキマイラ飼育記 メモ編

まだ続く。

  x:X |- P(x) :Type
 ------------------- パイ型形成子
   Πx∈X.P(x) :Type

  x:X |- f(x):P(x)
 ------------------- 依存ラムダ抽象
  Λx:X.f(x) : Πx:X.P(x)

  x:X |- A :Type
 ------------------- パイ型形成子
   Πx:X.A = X→A :Type

  x:X |- f(x):A 
 ------------------- ラムダ抽象
  λx:X.f(x): X→A

パラメータ領域Xを番号集合にすると：

  i:I |- Pi :Type
 ------------------- 非一様タプル型〈スキーマ〉形成子
   Πi∈I.Pi :Type

  i:I |- ai:Pi
 ------------------- 依存ラムダ抽象 タプルインスタンス構成
  Λi:I.ai : Πi:I.Pi

  i:I |- A :Type
 ------------------- 一様タプル型〈スキーマ〉形成子
   Πi:I.A = AI :Type

  i:I |- ai:A 
 ------------------- ラムダ抽象 リストインスタンス構成
  λi:I.ai: AI

型ファミリーPに沿った値ファミリー (x:X ⇒ f(x):P(x)) と型付きタプル (f(x))_x:X:Πx:X.P(x) を同一視しない。型ファミリーは（単一の）型ではなく、値ファミリーは（単一の）値ではない。しかし、型ファミリーのパイ型は型で、値ファミリーのタプルは値となる。

型ファミリーが型ではないことは、関手が対象ではないことと同じ。値ファミリーは単位にシュリンクする定数関手と型ファミリー関手のあいだの自然変換になる。

• 型＝圏の対象
• 型ファミリー＝離散圏からの関手
• 値ファミリー＝特殊な自然変換
• 型構成〈型形成〉＝極限
• 値〈データ〉構成＝極限にともなう自然変換の操作

たぶんまだ続く。