Nuprl Definition : universe-comp-fun

CompFun(A) ==  cop-to-cfun(compOp(A))


Definitions occuring in Statement :  universe-comp-op: compOp(t),  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)
FDL editor aliases :  universe-comp-fun
Latex:
CompFun(A)  ==    cop-to-cfun(compOp(A))


Date html generated: 2017_01_10-PM-00_08_25
Last ObjectModification: 2017_01_01-AM-11_51_42

Theory : cubical!type!theory


Home Index