~/dependentness/insane-pi { Ulf Norell's "insanely dependent" Pi: [x1 : A1, ..., xn : An] -> B, where every xi is in scope in every Ai, including its own. Must be fully applied. His prototype checker ties the knot lazily: types and terms are pointers to suspended closures, forced at the end. Source: https://github.com/UlfNorell/insane }

:dependentness

{ Ordinary Pi is the special case of insane Pi where each Ai may only mention earlier xj. Dropping the left-to-right restriction is strictly stronger: the repo's Sigma.agda encodes dependent pairs as a single function whose type mentions itself, f : (b : Bool) -> If A (B (f true)) b, and proves the projection laws by refl. }
~/dependent-type-theory 70:100 ~/insane-pi

{ Pure insane Pi looks like the floor of Eduardo's system, not its ceiling. Per his Sep 2026 post he still suspects insane Pi alone is enough but could not encode a proper algebra (dependent elimination, i.e. induction, over encoded data), so his theory carries more than pure insane Pi. The degree of self-reference is about the same; the gap is in what you can prove, so only a slight margin. }
~/insane-pi 90:100 ~/eduardorfs-type-theory