Nuprl Definition : universe-type

universe-type(t;I;a) ==  fst(t(a))


Definitions occuring in Statement :  cubical-term-at: u(a),  pi1: fst(t)
Definitions occuring in definition :  cubical-term-at: u(a),  pi1: fst(t)
FDL editor aliases :  universe-type
Latex:
universe-type(t;I;a)  ==    fst(t(a))


Date html generated: 2016_06_16-PM-05_23_48
Last ObjectModification: 2016_06_13-PM-06_37_27

Theory : cubical!type!theory


Home Index