Post #2669086
2026-04-13 11:14 UTC
@cxandru@types.pl using agda-categories over cubical also has the advantage that you can actually compile your programs
Replies (1)
-
@cxandru@types.pl 2026-04-13 11:21
@Taneb@hacksrus.xyz Only reason really is bc one of the applications is sorting with the Finite Multiset QIT as Index. The translation to stdlib of `IntrinsicallyRecursiveCoalgs` is entirely straightforward, I'm considering releasing a version that works for stdlib though idk what best practices are if one wanta to avoid code duplication …