formal.tex

simplify the circle rules
put unit, empty, and nat into U_0 instead of U_i, for emphasis
fix a reference for Peter and Thierry