アロー型と依存アロー型とパイ型

依存アロー型とパイ型は同じもの。アロー型=指数型は依存アロー型の特別なもの。

Lean 4 で依存アロー型の書き方が (x:α) → β (βは型項)となったが、Agdaでは以前からこの形だったようだ。

  • Π(x:α), β ≡ ∀(x:α), β ≡ (x:α)→β

カリー化/アンカリー化は同じようにできる。

  • Γ |-! (x:α)→β ⇔ Γ, (x:α) |-! β
  • Γ |-? (x:α)→β ⇔ Γ, (x:α) |-? β
  • Γ |- t^:(x:α)→β ⇔ Γ, (x:α) |-! t: β