Nuprl Definition : composition-term
comp cA [phi ⊢→ u] a0 ==
λI,rho. (cA I new-name(I) (s(rho);<new-name(I)>) phi(rho) (u)<(s(rho);<new-name(I)>)> o iota a0(rho))
Definitions occuring in Statement :
interval-type: 𝕀,
cc-adjoin-cube: (v;u),
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
cubical-term-at: u(a),
subset-iota: iota,
cubical-subset: I,psi,
face-presheaf: 𝔽,
csm-comp: G o F,
context-map: <rho>,
formal-cube: formal-cube(I),
cube-set-restriction: f(s),
nc-s: s,
new-name: new-name(I),
add-name: I+i,
dM_inc: <x>,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
apply: f a,
csm-ap-term: (t)s,
csm-comp: G o F,
cubical-subset: I,psi,
face-presheaf: 𝔽,
formal-cube: formal-cube(I),
subset-iota: iota,
context-map: <rho>,
cube-context-adjoin: X.A,
interval-type: 𝕀,
cc-adjoin-cube: (v;u),
cube-set-restriction: f(s),
add-name: I+i,
nc-s: s,
dM_inc: <x>,
new-name: new-name(I),
cubical-term-at: u(a)
FDL editor aliases :
composition-term
Latex:
comp cA [phi \mvdash{}\mrightarrow{} u] a0 ==
\mlambda{}I,rho. (cA I new-name(I) (s(rho);<new-name(I)>) phi(rho) (u)<(s(rho);<new-name(I)>)> o iota
a0(rho))
Date html generated:
2016_05_19-AM-10_19_46
Last ObjectModification:
2016_03_08-PM-02_07_42
Theory : cubical!type!theory
Home
Index