私が取り組んでいる形式化では、Unitタイプを、宇宙で定義されているAgda標準ライブラリからのSetような多形ライブラリに持ち上げる必要がありSet aます。
どうやってやるの？私はこのような別のタイプを定義できることを知っています：
record Unit {l} : Set l where
constructor unit
これは宇宙多型です。しかし、私はそれがこの問題に対するより慣用的な解決策を持っているべきだと信じています。誰かが私に解決策を提供できますか、それとも私に理由を説明する方法がない場合は？
実際、標準ライブラリを少し検索すると、Levelモジュールに必要なツールが見つかりました。解決策は、次のタイプを使用することですLift。
record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
constructor lift
field lower : A
ユニットタイプ
record ⊤ : Set where
constructor tt
を使用して、より高いユニバースレベルに持ち上げることができますLift ⊤。私は次の答えの一部を読んで解決策を見つけました。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加