Nuprl Definition : filling-uniformity
filling-uniformity(Gamma;A;fill) ==
∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}. ∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((fill I i rho phi u a0 rho g,i=j)
= (fill J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ A(g,i=j(rho)))
Definitions occuring in Statement :
cubical-path-0: cubical-path-0(Gamma;A;I;i;rho;phi;u),
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
subset-trans: subset-trans(I;J;f;x),
subset-iota: iota,
cubical-subset: I,psi,
face-presheaf: 𝔽,
csm-comp: G o F,
context-map: <rho>,
formal-cube: formal-cube(I),
cube-set-restriction: f(s),
I_cube: A(I),
nc-e': g,i=j,
nc-0: (i0),
nc-s: s,
add-name: I+i,
names-hom: I ⟶ J,
fset-member: a ∈ s,
fset: fset(T),
int-deq: IntDeq,
nat: ℕ,
all: ∀x:A. B[x],
not: ¬A,
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
fset: fset(T),
set: {x:A| B[x]} ,
nat: ℕ,
not: ¬A,
fset-member: a ∈ s,
int-deq: IntDeq,
names-hom: I ⟶ J,
I_cube: A(I),
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
csm-comp: G o F,
cubical-subset: I,psi,
formal-cube: formal-cube(I),
subset-iota: iota,
context-map: <rho>,
all: ∀x:A. B[x],
cubical-path-0: cubical-path-0(Gamma;A;I;i;rho;phi;u),
equal: s = t ∈ T,
cubical-type-at: A(a),
apply: f a,
csm-ap-term: (t)s,
subset-trans: subset-trans(I;J;f;x),
nc-e': g,i=j,
face-presheaf: 𝔽,
nc-s: s,
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s),
add-name: I+i,
nc-0: (i0)
FDL editor aliases :
filling-uniformity
Latex:
filling-uniformity(Gamma;A;fill) ==
\mforall{}I,J:fset(\mBbbN{}). \mforall{}i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\} . \mforall{}j:\{j:\mBbbN{}| \mneg{}j \mmember{} J\} . \mforall{}g:J {}\mrightarrow{} I. \mforall{}rho:Gamma(I+i). \mforall{}phi:\mBbbF{}(I).
\mforall{}u:\{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\}. \mforall{}a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((fill I i rho phi u a0 rho g,i=j)
= (fill J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g)))
Date html generated:
2016_05_19-AM-09_25_18
Last ObjectModification:
2015_11_09-PM-06_45_59
Theory : cubical!type!theory
Home
Index