シグマ型とパイ型

	用法1	用法2	用法3
シグマ型	依存ペア型	依存積型	依存和型
パイ型	依存関数型	依存指数型	依存積型

description _

procedure Sigma from a Type A and a Family (F : A → |Set|)
 produces a Type S
{
  // 省略
}

procedure Pi from a Type A and a Family (F : A → |Set|)
 produces a Type P
{
  // 省略
}

terminology _

vocabulary 依存型 {
  シグマ型 :=> the Sgima(A, F) for ( a Type A and a Family (F: A → |Set|) )
  パイ型 :=> the Pi(A, F) for ( a Type A and a Family (F: A → |Set|) )
  依存ペア := an element of (
    the Sgima(A, F) for ( a Type A and a Family (F: A → |Set|) )
  )
  依存関数 := an element of (
    the Pi(A, F) for ( a Type A and a Family (F: A → |Set|) )
  )
}

context 用法1 for 依存型 {
  依存ペア型 := シグマ型
  依存関数型 := パイ型
}

context 用法2 for 依存型 {
  依存積型 := シグマ型
  依存指数型 := パイ型
}

context 用法3 for 依存型 {
  依存和型 := シグマ型
  依存積型 := パイ型
}