rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> 
ext 
by intro universe 
.
H >> 
in 
by intro
where j<i.
Note that all the formation rules are intro rules for a universe type.
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
Currently there are no rules in the system for analyzing universes. At some later date such rules may be added.