Post #1467647
2026-04-19 20:32 UTC
does anyone (i'm mostly looking at @pigworker) have an implementation in runnable code for translating a strictly-positive inductive datatype to a container, i.e. the computational content of the attached corollary from "constructing strictly positive types"?
Replies (2)
-
@zanzi@mathstodon.xyz 2026-04-19 22:29
@chrisamaphone @pigworker me and @julesh have a bunch of lambda and sequent calculi implemented for the category of containers, but would need to check which of them are public
-
@mevenlennonbertrand@lipn.info 2026-04-20 06:47
@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)