~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