Can Axiomatic Systems Have a Geometry and a Type?

A Saturday reflection on imagining a geometry of axiomatic systems and wondering whether theories could become types that carry information about what can and can't be proven about them, inspired by proof assistants like Lean.