Nuprl Definition : cubical-path-condition'
cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1) ==
∀J:fset(ℕ). ∀f:I,phi(J). ((a1 (i1)(rho) f) = u((i1) ⋅ f) ∈ A(f((i1)(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-1: (i1),
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-1: (i1)
FDL editor aliases :
cubical-path-condition'
Latex:
cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1) ==
\mforall{}J:fset(\mBbbN{}). \mforall{}f:I,phi(J). ((a1 (i1)(rho) f) = u((i1) \mcdot{} f))
Date html generated:
2016_05_19-AM-09_18_17
Last ObjectModification:
2015_11_03-AM-00_30_11
Theory : cubical!type!theory
Home
Index