A fairly general way to describe a geometric object in b-rep format is as a layered directed graph with the description of each face associated with a node. (The base layer of the graph is the 0-dimensional faces, i.e., vertices, and successive layers specify higher-dimensional faces.) For polyhedral objects, the information associated with each node is a system of linear equations that define the affine hull of the face. S. Allen showed how to define this layered structure in Nuprl with a few lines of Nuprl terms with bindings. Allen's type definition also yields a notation for specifying any particular instance of an n-dimension polyhedral object. The notation is a simple recursive nesting with the 0-dimensional faces defined by the outermost layer of nesting, and then higher dimensions are nested inside.
Vavasis has adopted Allen's notation to describe the geometry of the input domain for his n-dimensional mesh generator. There are many correctness properties associated with a polyhedral region that could be completely captured by theorems in Nuprl.
For Chew's surface mesher, the layered structure can also be used, but the faces are now defined by nonlinear equations, typically algebraic. The correctness properties for a boundary-rep object with nonlinear faces are much more difficult to verify, but fortunately Nuprl and Weyl provide exactly the right environment for this problem. (The heart of the correctness testing involves checking for intersections between algebraic surfaces.)