問題タブ [agda]

言うまでもなく、Haskell の標準的な構造は

素晴らしく、非常に便利です。

Agdaで同様のものを定義しようとしています（完全を期すために記載します）

fは厳密に正であるとは限らないため、失敗します。これは理にかなっています。適切に選択することで、この構造から簡単に矛盾を得ることができます。

私の質問は次のとおりです。Agda で再帰スキームをエンコードする希望はありますか? それは行われましたか？何が必要ですか？

これが math.SE の質問なのか SO の質問なのかについては、私はやや未定でしたが、Haskell プログラマーはよく知っているかもしれないのに対し、一般の数学者は特にこのカテゴリについてあまり知らないか気にかけているとは思えません。

したがって、 Haskには多かれ少なかれ製品があることがわかっています (もちろん、ここでは理想化された Hask を使用しています)。イコライザーがあるかどうかに興味があります (その場合、すべての有限の制限があります)。

セットのように分離を行うことができないため、直感的にはそうではないように思われます。そのため、サブオブジェクトは一般的に構築するのが難しいようです。しかし、思いつきたい特定のケースについては、Setでイコライザーを作成してカウントすることでハックできるようです (結局のところ、すべての Haskell 型は可算であり、すべての可算セットはHaskell が持つ有限型または自然型のいずれかに同型)。そのため、反例を見つける方法がわかりません。

さて、Agda はもう少し有望に思えます: サブオブジェクトを形成するのは比較的簡単です。明らかなシグマ型Σ A (λ x → f x == g x)はイコライザーですか? 詳細がうまくいかない場合、それは道徳的にイコライザーですか？

Agdaで、同じ長さでなければならないベクトルのペアを定義するにはどうすればよいですか？

Agda で型階層がどのように機能するかを理解しようとしています。

セット型 X を定義するとします。

そして、誘導型の構築に進みます

の型はX -> Set何ですか? それはセットですか、それともタイプですか？

ありがとうございました！