@mevenlennonbertrand@lipn.info
Post #1780149
2026-04-20 06:47 UTC
@chrisamaphone @pigworker There are some bits of this formalised in Agda, as reported in https://arxiv.org/abs/2409.02603 (iirc the paper focuses on the fixed point part, but the formalisation does more)
Replies (2)
-
@pigworker@types.pl 2026-04-20 07:54
@mevenlennonbertrand Cool! @chrisamaphone I’m sure I’ve done variants on this construction a number of times, but I’m struggling to find the files. It’s more fiddly than it should be, for essentially bureaucratic reasons.
-
@chrisamaphone@hci.social 2026-04-20 14:48
@mevenlennonbertrand @pigworker thanks Meven!