Nuprl Definition : cubical-bool
Bool == encode(discr(𝔹);discrete-comp(();𝔹))
Definitions occuring in Statement :
universe-encode: encode(T;cT),
discrete-comp: discrete-comp(G;T),
discrete-cubical-type: discr(T),
trivial-cube-set: (),
bool: 𝔹
Definitions occuring in definition :
bool: 𝔹,
trivial-cube-set: (),
discrete-comp: discrete-comp(G;T),
discrete-cubical-type: discr(T),
universe-encode: encode(T;cT)
FDL editor aliases :
cubical-bool
Latex:
Bool == encode(discr(\mBbbB{});discrete-comp(();\mBbbB{}))
Date html generated:
2017_02_21-AM-11_03_51
Last ObjectModification:
2017_02_13-PM-04_47_20
Theory : cubical!type!theory
Home
Index