Nuprl Definition : cubical-subset
I,psi == rep-sub-sheaf(CubeCat;I;λJ,f. (psi f) = 1)
Definitions occuring in Statement :
name-morph-satisfies: (psi f) = 1,
cube-cat: CubeCat,
rep-sub-sheaf: rep-sub-sheaf(C;X;P),
lambda: λx.A[x]
Definitions occuring in definition :
rep-sub-sheaf: rep-sub-sheaf(C;X;P),
cube-cat: CubeCat,
lambda: λx.A[x],
name-morph-satisfies: (psi f) = 1
FDL editor aliases :
cubical-subset
Latex:
I,psi == rep-sub-sheaf(CubeCat;I;\mlambda{}J,f. (psi f) = 1)
Date html generated:
2018_05_23-AM-08_40_42
Last ObjectModification:
2018_02_23-PM-08_57_32
Theory : cubical!type!theory
Home
Index