Nuprl Definition : cubical-fun-family
cubical-fun-family(X; A; B; I; a) ==
{w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A(f(a)) ⟶ B(f(a))|
∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f(a)). ((w J f u f(a) g) = (w K f ⋅ g (u f(a) g)) ∈ B(g(f(a))))}
Definitions occuring in Statement :
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
cube-set-restriction: f(s),
nh-comp: g ⋅ f,
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],
equal: s = t ∈ T,
cubical-type-at: A(a),
apply: f a,
nh-comp: g ⋅ f,
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s)
Latex:
cubical-fun-family(X; A; B; I; a) ==
\{w:J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I {}\mrightarrow{} u:A(f(a)) {}\mrightarrow{} B(f(a))|
\mforall{}J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}u:A(f(a)). ((w J f u f(a) g) = (w K f \mcdot{} g (u f(a) g)))\}
Date html generated:
2016_05_18-PM-01_45_29
Last ObjectModification:
2016_02_21-PM-10_02_42
Theory : cubical!type!theory
Home
Index