Nuprl Definition : comp-fun-to-comp-op

comp-fun-to-comp-op(Gamma;A;comp) ==  λI,i,rho,phi,u,a0. comp-fun-to-comp-op1(Gamma;A;comp) I i rho phi u a0(1)


Definitions occuring in Statement :  comp-fun-to-comp-op1: comp-fun-to-comp-op1(Gamma;A;comp),  cubical-term-at: u(a),  nh-id: 1,  apply: f a,  lambda: λx.A[x]
Definitions occuring in definition :  lambda: λx.A[x],  cubical-term-at: u(a),  apply: f a,  comp-fun-to-comp-op1: comp-fun-to-comp-op1(Gamma;A;comp),  nh-id: 1
FDL editor aliases :  comp-fun-to-comp-op
Latex:
comp-fun-to-comp-op(Gamma;A;comp)  ==
    \mlambda{}I,i,rho,phi,u,a0.  comp-fun-to-comp-op1(Gamma;A;comp)  I  i  rho  phi  u  a0(1)


Date html generated: 2016_05_19-AM-10_36_19
Last ObjectModification: 2016_03_28-PM-05_56_54

Theory : cubical!type!theory


Home Index