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