これはagdaの従属関数型の有効な定義ではないのはなぜですか？

Question

私は講師がAgdaでPiタイプを定義することは不可能である、または少なくとも非常に難しいと述べた講義を見ていました。しかし、私は方法がなければならないと確信しています。宇宙の型と宇宙型から宇宙型を考えると、その型から家族型の何らかの関数はPi型になります。だから私はそれがラムダを使用することを意味するだろうと思った：

data Pi (A : Set) (B : A -> Set) : Set where 
    \ (a : A) -> (b : B a) : Pi A B 

私はこれをロードしようとすると、それは私にパースエラーが発生します。私はなぜ、おそらく\が型コンストラクタであることを望まないが、ラムダが関数型の型コンストラクタであると考えるのは当然のことです。 EmacsでAgdaにラテックス機能を使用していますが、スタックオーバーフローでラテックスを書くことはできません。つまり、小文字のラムダを大文字のラムダに置き換えて、ユニークな型のコンストラクタが必要かどうかを確認しましたが、役に立たなかったのです。

Answer 1

あなたは「パイ型を定義する」とはどういう意味ですかそれは

data Pi (A : Set) (B : A -> Set) : Set where 
    Λ : ((a : A) -> B a) -> Pi A B