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