依存アロー型とパイ型は同じもの。アロー型=指数型は依存アロー型の特別なもの。
Lean 4 で依存アロー型の書き方が (x:α) → β (βは型項)となったが、Agdaでは以前からこの形だったようだ。
- Π(x:α), β ≡ ∀(x:α), β ≡ (x:α)→β
カリー化/アンカリー化は同じようにできる。
- Γ |-! (x:α)→β ⇔ Γ, (x:α) |-! β
- Γ |-? (x:α)→β ⇔ Γ, (x:α) |-? β
- Γ |- t^:(x:α)→β ⇔ Γ, (x:α) |-! t: β