Nuprl Definition : filling-op
filling-op(Gamma;A) ==
{fill:I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ 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)
⟶ {a:A(rho)|
(section-iota(Gamma;A;I+i;rho;a) = u ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}) ∧ ((a rho (i0)) = a0 ∈ A((i0)(rho)))} |
filling-uniformity(Gamma;A;fill)}
Definitions occuring in Statement :
filling-uniformity: filling-uniformity(Gamma;A;fill),
cubical-path-0: cubical-path-0(Gamma;A;I;i;rho;phi;u),
section-iota: section-iota(Gamma;A;I;rho;a),
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
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-0: (i0),
nc-s: s,
add-name: I+i,
fset-member: a ∈ s,
fset: fset(T),
int-deq: IntDeq,
nat: ℕ,
not: ¬A,
and: P ∧ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
fset: fset(T),
nat: ℕ,
not: ¬A,
fset-member: a ∈ s,
int-deq: IntDeq,
I_cube: A(I),
function: x:A ⟶ B[x],
cubical-path-0: cubical-path-0(Gamma;A;I;i;rho;phi;u),
set: {x:A| B[x]} ,
and: P ∧ Q,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
csm-comp: G o F,
cubical-subset: I,psi,
face-presheaf: 𝔽,
nc-s: s,
formal-cube: formal-cube(I),
subset-iota: iota,
context-map: <rho>,
section-iota: section-iota(Gamma;A;I;rho;a),
equal: s = t ∈ T,
cubical-type-at: A(a),
cube-set-restriction: f(s),
cubical-type-ap-morph: (u a f),
add-name: I+i,
nc-0: (i0),
filling-uniformity: filling-uniformity(Gamma;A;fill)
FDL editor aliases :
filling-op
Latex:
filling-op(Gamma;A) ==
\{fill:I:fset(\mBbbN{})
{}\mrightarrow{} i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\}
{}\mrightarrow{} rho:Gamma(I+i)
{}\mrightarrow{} phi:\mBbbF{}(I)
{}\mrightarrow{} u:\{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\}
{}\mrightarrow{} a0:cubical-path-0(Gamma;A;I;i;rho;phi;u)
{}\mrightarrow{} \{a:A(rho)| (section-iota(Gamma;A;I+i;rho;a) = u) \mwedge{} ((a rho (i0)) = a0)\} |
filling-uniformity(Gamma;A;fill)\}
Date html generated:
2016_05_19-AM-09_25_34
Last ObjectModification:
2016_01_26-PM-06_30_46
Theory : cubical!type!theory
Home
Index