Is there a version of Mitchell-Benabou language for internal categories in toposes (with natural number objects)? What I have in mind is something that will allow automatic translations of definitions and proofs to internal categories that gives the expected results for established notions. [I have glanced through "Relative set theories", and the relevant chapters of Jacobs, "Categorical logic and type theory"; they do not seem to what I am looking for, in the sense that the primary focus is not on the properties of the internal category.] Thanks in advance Nath Rao