きゅーけー@tojoqk@mastodon.tojo.tokyo: ようやく欲しい物をみつけた。Function.Bundles にあったのか。。。<br><br> _⤖_ : Set a → Set b → Set _<br>A ⤖ B = Bijection (≡.setoid A) (≡.setoid B)

Home | Notifications | New Note | Local | Federated | Search | Logout

Note Detail

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-22 21:44:47)
TypeScript の as const で定義して定数配列から Union 型を作るやつ、あれと同じこと Agda でやりたいけどやり方わからないなあ〜とずっと思っていたけど完全に解決した。

そもそも要素の重複のない長さnの配列というものは Fin n と同型であり、Agda でそれを実現するには Fin n で定義して、それぞれの要素にドメインに沿った別名をつければいいんだ。。。

そしてこれは既に Gregorianum ライブラリで曜日を定義するにあたってやってた。今後列挙する機会のあるユニオン型を定義したいときは最初から Fin n を使って定義しようと思う。
https://github.com/tojoqk/gregorianum/blob/main/src/Gregorianum/Date/Weekday.agda
---Reply---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-22 23:45:20)
ようやく欲しい物をみつけた。Function.Bundles にあったのか。。。

 _⤖_ : Set a → Set b → Set _
A ⤖ B = Bijection (≡.setoid A) (≡.setoid B)


---Replies---

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-22 23:49:38)
ほしいのこっちっぽいな。。。

_↔_ : Set a → Set b → Set _
A ↔ B = Inverse (≡.setoid A) (≡.setoid B)