Nuprl Definition : cubical-type-restriction
cubical-type-restriction(X;T;I,a,x.psi[I; a; x]) ==
∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I). ∀x:T(a). (psi[I; a; x] ⇒ psi[J; f(a); (x a f)])
Definitions occuring in Statement :
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
cube-set-restriction: f(s),
I_cube: A(I),
names-hom: I ⟶ J,
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
fset: fset(T),
nat: ℕ,
names-hom: I ⟶ J,
I_cube: A(I),
all: ∀x:A. B[x],
cubical-type-at: A(a),
implies: P ⇒ Q,
cube-set-restriction: f(s),
cubical-type-ap-morph: (u a f)
FDL editor aliases :
cubical-type-restriction
Latex:
cubical-type-restriction(X;T;I,a,x.psi[I; a; x]) ==
\mforall{}I,J:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}a:X(I). \mforall{}x:T(a). (psi[I; a; x] {}\mRightarrow{} psi[J; f(a); (x a f)])
Date html generated:
2016_06_16-PM-01_40_30
Last ObjectModification:
2016_06_02-PM-09_26_33
Theory : cubical!type!theory
Home
Index