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