Foundational systems are by nature adequate in principle for formalizing a large body (if not all) of informal mathematical knowledge. However, the formalizations usually proceed by means of various encodings, which may be adequate for some mathematical purposes but not very faithful semantically or readable to a human being. For example, what does the formalization of the definition of a Lie group look like? Is it recognizable as such? I will exhibit a system which is designed from the ground up to be give rise to simple, readable formalizations that minimize encoding overhead. The goal is to show that not only is it possible to do this, but it is possible to do so with only a few very simple primitives. The system bears some resemblance to, and is partly inspired by, constructive type theories such as that of Martin-L, NUPRL's type theory, homotopy type theory, and the calculus of inductive constructions (which is used by Coq). I will illustrate the use of the system by formalizing a few basic theorems, and discuss the possible applications of the approach, and its drawbacks. This work is preliminary and I am eager to solicit feedback from other logicians, so I will leave plenty of time at the end for questions, discussion, and criticism.