Nuprl Definition : csm-comp-structure
(cA)tau == λH,sigma,phi,u,a0. (cA H tau o sigma phi u a0)
Definitions occuring in Statement :
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-comp: G o F,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-comp: G o F,
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
csm-comp-structure
Latex:
(cA)tau == \mlambda{}H,sigma,phi,u,a0. (cA H tau o sigma phi u a0)
Date html generated:
2016_05_19-AM-10_40_46
Last ObjectModification:
2016_04_14-AM-10_38_45
Theory : cubical!type!theory
Home
Index