Post #1846837
2026-04-28 07:44 UTC
@jeanas @mevenlennonbertrand @jpoiret @carloangiuli Thanks for sharing this! I think I haven’t seen it yet.
Replies (1)
-
@mevenlennonbertrand@lipn.info 2026-04-28 07:55
@jonmsterling @jeanas @jpoiret @carloangiuli The core idea is perhaps unsurprising: if you only quote close normal forms, everything is fine wrt to congruence. Still, this gives a very direct construction for "relevant" CT (the one with a Sigma type).