Post #3066771
2026-05-21 16:03 UTC
@mc@mathstodon.xyz Yeah exactly, you need a well-behaved notion of definitional equality in order to elaborate
Replies (1)
-
@olynch@mathstodon.xyz 2026-05-21 16:08
@mc@mathstodon.xyz That's what I say when people only give me a notion of isomorphism between types, I'm like "uh elaborate please" and then they can't, and are rekked.