~dependentness { Ranking all types of type theory by how dependent they are. }

~/dependentness/normal-type-theory { Simply-typed and polymorphic lambda calculi. Types do not depend on terms. }
~/dependentness/dependent-type-theory { Pi and Sigma types. Types depend on terms. }
~/dependentness/eduardorfs-type-theory { "Insanely" dependent type theory. ~1y to grasp DTT, ~4y to push this edge. }

:dependentness

{ it's insanely dependent }
~/dependent-type-theory 67:100 ~/eduardorfs-type-theory

{ Normal type theory has little dependentness }
~/dependent-type-theory 100:50 ~/normal-type-theory

~/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