Nuprl Definition : glue-type

Glue [phi ⊢→ (T;w)] ==  <λI,rho. glue-cube(Gamma;A;phi;T;w;I;rho), λI,J,f,rho,u. glue-morph(Gamma;A;phi;T;w;I;rho;J;f;\000Cu)>



Definitions occuring in Statement :  glue-morph: glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u) glue-cube: glue-cube(Gamma;A;phi;T;w;I;rho) lambda: λx.A[x] pair: <a, b>
Definitions occuring in definition :  pair: <a, b> glue-cube: glue-cube(Gamma;A;phi;T;w;I;rho) lambda: λx.A[x] glue-morph: glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u)
FDL editor aliases :  glue-type

Latex:
Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A  ==
    <\mlambda{}I,rho.  glue-cube(Gamma;A;phi;T;w;I;rho),  \mlambda{}I,J,f,rho,u.  glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u)>



Date html generated: 2016_05_20-AM-08_44_43
Last ObjectModification: 2016_02_25-AM-01_26_14

Theory : cubical!type!theory


Home Index