Nuprl Definition : constant-cubical-type
(X) == <λI,alpha. X(I), λI,J,f,alpha,w. f(w)>
Wellformedness Lemmas :
constant-cubical-type_wf
Definitions occuring in Statement :
cube-set-restriction: f(s),
I-cube: X(I),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
I-cube: X(I),
lambda: λx.A[x],
cube-set-restriction: f(s)
FDL editor aliases :
constant-cubical-type
constant-cubical-type
Latex:
(X) == <\mlambda{}I,alpha. X(I), \mlambda{}I,J,f,alpha,w. f(w)>
Date html generated:
2016_06_16-PM-05_48_09
Last ObjectModification:
2015_09_23-AM-09_30_58
Theory : cubical!sets
Home
Index