Nuprl Definition : discrete-cubical-type

discr(T) ==  <λI,alpha. T, λI,J,f,alpha,x. x>



Wellformedness Lemmas :  discrete-cubical-type_wf
Definitions occuring in Statement :  lambda: λx.A[x] pair: <a, b>
Definitions occuring in definition :  pair: <a, b> lambda: λx.A[x]
FDL editor aliases :  discrete-cubical-type discrete-cubical-type

Latex:
discr(T)  ==    <\mlambda{}I,alpha.  T,  \mlambda{}I,J,f,alpha,x.  x>



Date html generated: 2016_06_16-PM-05_47_53
Last ObjectModification: 2015_09_23-AM-09_30_54

Theory : cubical!sets


Home Index