Nuprl Definition : glue-cube
glue-cube(Gamma;A;phi;T;w;I;rho) ==
if (phi(rho)==1)
then T(rho)
else {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))} ⟶ T(f(rho)) × A(rho)|
let t,a = ta
in glue-equations(Gamma;A;phi;T;w;I;rho;t;a)}
fi
Definitions occuring in Statement :
glue-equations: glue-equations(Gamma;A;phi;T;w;I;rho;t;a),
cubical-term-at: u(a),
cubical-type-at: A(a),
fl-eq: (x==y),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
names-hom: I ⟶ J,
lattice-1: 1,
lattice-point: Point(l),
fset: fset(T),
nat: ℕ,
ifthenelse: if b then t else f fi ,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
equal: s = t ∈ T
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
fl-eq: (x==y),
product: x:A × B[x],
fset: fset(T),
nat: ℕ,
function: x:A ⟶ B[x],
set: {x:A| B[x]} ,
names-hom: I ⟶ J,
equal: s = t ∈ T,
lattice-point: Point(l),
cubical-term-at: u(a),
lattice-1: 1,
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
cubical-type-at: A(a),
spread: spread def,
glue-equations: glue-equations(Gamma;A;phi;T;w;I;rho;t;a)
FDL editor aliases :
glue-cube
Latex:
glue-cube(Gamma;A;phi;T;w;I;rho) ==
if (phi(rho)==1)
then T(rho)
else \{ta:J:fset(\mBbbN{}) {}\mrightarrow{} f:\{f:J {}\mrightarrow{} I| phi(f(rho)) = 1\} {}\mrightarrow{} T(f(rho)) \mtimes{} A(rho)|
let t,a = ta
in glue-equations(Gamma;A;phi;T;w;I;rho;t;a)\}
fi
Date html generated:
2016_05_19-AM-11_15_29
Last ObjectModification:
2016_02_24-PM-05_51_44
Theory : cubical!type!theory
Home
Index