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

Note Detail

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

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

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