Nuprl Definition : composition-term

comp cA [phi ⊢→ u] a0 ==
  λI,rho. (cA new-name(I) (s(rho);<new-name(I)>phi(rho) (u)<(s(rho);<new-name(I)>)> 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: 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: a lambda: λx.A[x]
Definitions occuring in definition :  lambda: λx.A[x] apply: a csm-ap-term: (t)s csm-comp: 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