Nuprl Definition : comp-fun-to-comp-op1
comp-fun-to-comp-op1(Gamma;A;comp) ==
λI,i,rho,phi,u,a0. (comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();𝔽;I;⋅;phi) (u)cube+(I;i)
canonical-section(Gamma;A;I;(i0)(rho);a0))
Definitions occuring in Statement :
face-type: 𝔽,
cube+: cube+(I;i),
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
canonical-section: canonical-section(Gamma;A;I;rho;a),
csm-comp: G o F,
context-map: <rho>,
trivial-cube-set: (),
formal-cube: formal-cube(I),
cube-set-restriction: f(s),
nc-0: (i0),
add-name: I+i,
it: ⋅,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
apply: f a,
csm-comp: G o F,
cube-context-adjoin: X.A,
interval-type: 𝕀,
formal-cube: formal-cube(I),
context-map: <rho>,
trivial-cube-set: (),
face-type: 𝔽,
it: ⋅,
csm-ap-term: (t)s,
cube+: cube+(I;i),
canonical-section: canonical-section(Gamma;A;I;rho;a),
cube-set-restriction: f(s),
add-name: I+i,
nc-0: (i0)
FDL editor aliases :
comp-fun-to-comp-op1
Latex:
comp-fun-to-comp-op1(Gamma;A;comp) ==
\mlambda{}I,i,rho,phi,u,a0. (comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();\mBbbF{};I;\mcdot{};phi)
(u)cube+(I;i)
canonical-section(Gamma;A;I;(i0)(rho);a0))
Date html generated:
2016_05_19-AM-10_35_53
Last ObjectModification:
2016_03_28-PM-05_52_02
Theory : cubical!type!theory
Home
Index