Nuprl Definition : cubical-term
{X ⊢ _:A} == {u:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)| ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I). ((u I a a f) = (u J f(a)) ∈ A(f(a)))}
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],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
fset: fset(T),
nat: ℕ,
names-hom: I ⟶ J,
all: ∀x:A. B[x],
I_cube: A(I),
equal: s = t ∈ T,
cubical-type-at: A(a),
cubical-type-ap-morph: (u a f),
apply: f a,
cube-set-restriction: f(s)
FDL editor aliases :
cubical-term
cubical-term
Latex:
\{X \mvdash{} \_:A\} ==
\{u:I:fset(\mBbbN{}) {}\mrightarrow{} a:X(I) {}\mrightarrow{} A(a)| \mforall{}I,J:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}a:X(I). ((u I a a f) = (u J f(a)))\}
Date html generated:
2016_05_18-PM-01_40_16
Last ObjectModification:
2015_11_05-PM-02_23_33
Theory : cubical!type!theory
Home
Index