Nuprl Definition : cubical-path-condition
cubical-path-condition(Gamma;A;I;i;rho;phi;u;a0) ==
∀J:fset(ℕ). ∀f:I,phi(J). ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
Definitions occuring in Statement :
cubical-term-at: u(a),
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
cubical-subset: I,psi,
cube-set-restriction: f(s),
I_cube: A(I),
nc-0: (i0),
add-name: I+i,
nh-comp: g ⋅ f,
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
equal: s = t ∈ T
Definitions occuring in definition :
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
I_cube: A(I),
cubical-subset: I,psi,
equal: s = t ∈ T,
cubical-type-at: A(a),
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s),
add-name: I+i,
cubical-term-at: u(a),
nh-comp: g ⋅ f,
nc-0: (i0)
FDL editor aliases :
cubical-path-condition
Latex:
cubical-path-condition(Gamma;A;I;i;rho;phi;u;a0) ==
\mforall{}J:fset(\mBbbN{}). \mforall{}f:I,phi(J). ((a0 (i0)(rho) f) = u((i0) \mcdot{} f))
Date html generated:
2016_05_19-AM-09_17_07
Last ObjectModification:
2015_11_03-AM-00_16_16
Theory : cubical!type!theory
Home
Index