Formal Representation of Mathematics in a Dependently Typed Set Theory