Elektrine lite

← Feed

@Taneb@hacksrus.xyz

Post #2669085

2026-04-13 10:26 UTC

@cxandru@types.pl any reason this is using cubical for its definition of categories rather than agda-categories (which I think works better with stdlib)?

Replies (1)

  • @Taneb@hacksrus.xyz 2026-04-13 11:14

    @cxandru@types.pl using agda-categories over cubical also has the advantage that you can actually compile your programs

    Open ##2669086