I have a small amount of familiarity with type theory, from having read parts of
Principia Mathematica. But most of that was years ago. Furthermore and perhaps more importantly, I have made no effort to write in a way that captures how one expresses things in type theory,
and I have overly simplified types
by identifying them with integers.