Nuprl Definition : cubical-isect-family
cubical-isect-family(X;A;B;I;a) ==
{w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ (⋂u:A(f(a)). B((f(a);u)))|
∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f(a)). ((w J f (f(a);u) g) = (w K f ⋅ g) ∈ B(g((f(a);u))))}
Definitions occuring in Statement :
cc-adjoin-cube: (v;u),
cube-context-adjoin: X.A,
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,
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
nh-comp: g ⋅ f,
apply: f a,
cube-set-restriction: f(s),
cc-adjoin-cube: (v;u),
cubical-type-ap-morph: (u a f),
cube-context-adjoin: X.A,
cubical-type-at: A(a),
equal: s = t ∈ T,
all: ∀x:A. B[x],
names-hom: I ⟶ J,
nat: ℕ,
fset: fset(T),
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
set: {x:A| B[x]}
FDL editor aliases :
cubical-isect-family
Latex:
cubical-isect-family(X;A;B;I;a) ==
\{w:J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I {}\mrightarrow{} (\mcap{}u:A(f(a)). B((f(a);u)))|
\mforall{}J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}u:A(f(a)). ((w J f (f(a);u) g) = (w K f \mcdot{} g))\}
Date html generated:
2016_07_08-PM-10_38_04
Last ObjectModification:
2016_07_08-AM-11_52_46
Theory : cubical!type!theory
Home
Index