Nuprl Definition : cubical-pi-family
cubical-pi-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 u (f(a);u) g) = (w K f ⋅ g (u f(a) 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,
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),
cube-context-adjoin: X.A,
cc-adjoin-cube: (v;u),
apply: f a,
nh-comp: g ⋅ f,
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s)
FDL editor aliases :
cubical-pi-family
cubical-pi-family
Latex:
cubical-pi-family(X;A;B;I;a) ==
\{w:J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I {}\mrightarrow{} u:A(f(a)) {}\mrightarrow{} 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 u (f(a);u) g) = (w K f \mcdot{} g (u f(a) g)))\}
Date html generated:
2016_05_18-PM-01_44_57
Last ObjectModification:
2015_10_29-AM-00_22_48
Theory : cubical!type!theory
Home
Index