Nuprl Definition : glue-type
Glue [phi ⊢→ (T;w)] A == <λ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