Nuprl Definition : glue-equations
glue-equations(Gamma;A;phi;T;w;I;rho;t;a) ==
(∀J:fset(ℕ). ∀f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))} . ∀K:fset(ℕ). ∀g:K ⟶ J.
((t J f f(rho) g) = (t K f ⋅ g) ∈ T(f ⋅ g(rho))))
∧ (∀J:fset(ℕ). ∀f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))} .
((w(f(rho)) J 1 (t J f)) = (a rho f) ∈ A(f(rho))))
Definitions occuring in Statement :
cubical-term-at: u(a),
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
nh-comp: g ⋅ f,
nh-id: 1,
names-hom: I ⟶ J,
lattice-1: 1,
lattice-point: Point(l),
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
nh-comp: g ⋅ f,
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
names-hom: I ⟶ J,
lattice-point: Point(l),
lattice-1: 1,
face_lattice: face_lattice(I),
equal: s = t ∈ T,
cubical-type-at: A(a),
cubical-term-at: u(a),
cube-set-restriction: f(s),
nh-id: 1,
apply: f a,
cubical-type-ap-morph: (u a f)
FDL editor aliases :
glue-equations
Latex:
glue-equations(Gamma;A;phi;T;w;I;rho;t;a) ==
(\mforall{}J:fset(\mBbbN{}). \mforall{}f:\{f:J {}\mrightarrow{} I| phi(f(rho)) = 1\} . \mforall{}K:fset(\mBbbN{}). \mforall{}g:K {}\mrightarrow{} J.
((t J f f(rho) g) = (t K f \mcdot{} g)))
\mwedge{} (\mforall{}J:fset(\mBbbN{}). \mforall{}f:\{f:J {}\mrightarrow{} I| phi(f(rho)) = 1\} . ((w(f(rho)) J 1 (t J f)) = (a rho f)))
Date html generated:
2016_05_19-AM-11_15_07
Last ObjectModification:
2016_02_25-PM-04_45_51
Theory : cubical!type!theory
Home
Index