Nuprl Definition : univ-trans
univ-trans(G;T) == transprt-fun(G;decode(T);cop-to-cfun(compOp(T)))
Definitions occuring in Statement :
universe-comp-op: compOp(t),
universe-decode: decode(t),
transprt-fun: transprt-fun(Gamma;A;cA),
comp-op-to-comp-fun: cop-to-cfun(cA)
Definitions occuring in definition :
universe-comp-op: compOp(t),
comp-op-to-comp-fun: cop-to-cfun(cA),
universe-decode: decode(t),
transprt-fun: transprt-fun(Gamma;A;cA)
FDL editor aliases :
univ-trans
Latex:
univ-trans(G;T) == transprt-fun(G;decode(T);cop-to-cfun(compOp(T)))
Date html generated:
2017_01_10-PM-00_23_15
Last ObjectModification:
2017_01_02-PM-01_04_54
Theory : cubical!type!theory
Home
Index