Nuprl Definition : closed-cubical-term
closed-cubical-term(T) ==
{u:I:fset(ℕ) ⟶ ((fst(T)) I)| ∀I,J:fset(ℕ). ∀f:J ⟶ I. (((snd(T)) I J f (u I)) = (u J) ∈ ((fst(T)) J))}
Definitions occuring in Statement :
names-hom: I ⟶ J,
fset: fset(T),
nat: ℕ,
pi1: fst(t),
pi2: snd(t),
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: ℕ,
all: ∀x:A. B[x],
names-hom: I ⟶ J,
equal: s = t ∈ T,
pi1: fst(t),
pi2: snd(t),
apply: f a
FDL editor aliases :
closed-cubical-term
Latex:
closed-cubical-term(T) ==
\{u:I:fset(\mBbbN{}) {}\mrightarrow{} ((fst(T)) I)| \mforall{}I,J:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. (((snd(T)) I J f (u I)) = (u J))\}
Date html generated:
2020_05_20-PM-01_52_41
Last ObjectModification:
2020_03_20-PM-00_33_20
Theory : cubical!type!theory
Home
Index