きゅーけー@tojoqk@mastodon.tojo.tokyo: ほしいのこっちっぽいな。。。<br><br>_↔_ : Set a → Set b → Set _<br>A ↔ B = Inverse (≡.setoid A) (≡.setoid B)

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

Note Detail

Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-22 23:45:20)
ようやく欲しい物をみつけた。Function.Bundles にあったのか。。。

 _⤖_ : Set a → Set b → Set _
A ⤖ B = Bijection (≡.setoid A) (≡.setoid B)
---Reply---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-22 23:49:38)
ほしいのこっちっぽいな。。。

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


---Replies---

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-23 00:36:13)
Agdaの標準ライブラリにあるの同型の定義を使った。すばらしい。
https://github.com/tojoqk/gregorianum/commit/4beaa459cc1a27fce4982ca15e2b46efcf486454