I discuss how to define internalized relational typings, implicit products, and two forms of natural number types, in RelTT.