Nuprl - Some Definitions

action_set	`Def ActionSet(T) == car:TypeTcarcar` `Thm* T:Type{i}. ActionSet(T) Type{i'}`
aset_act	`Def a.act == 2of(a)` `Thm* T:Type, a:ActionSet(T). a.act Ta.cara.car`
aset_car	`Def a.car == 1of(a)` `Thm* T:Type, a:ActionSet(T). a.car Type`
pi2	`Def 2of(t) == t.2` `Thm* A:Type, B:(AType), p:a:AB(a). 2of(p) B(1of(p))`
pi1	`Def 1of(t) == t.1` `Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A`

About: