Nuprl Definition : constant-cubical-type
(X) == <λI,alpha. X(I), λI,J,f,alpha,w. f(w)>
Definitions occuring in Statement :
cube-set-restriction: f(s),
I_cube: A(I),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
I_cube: A(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_05_18-PM-01_57_30
Last ObjectModification:
2015_10_28-PM-06_31_30
Theory : cubical!type!theory
Home
Index