Nuprl Definition : uniform-filling-function
uniform-filling-function{j:l, i:l}(Gamma;A;fill) ==
∀H,K:j⊢. ∀tau:K j⟶ H. ∀sigma:H.𝕀 j⟶ Gamma. ∀phi:{H ⊢ _:𝔽}. ∀u:{H.𝕀, (phi)p ⊢ _:(A)sigma}.
∀a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}.
((fill H sigma phi u a0)tau+ = (fill K sigma o tau+ (phi)tau (u)tau+ (a0)tau) ∈ {K.𝕀 ⊢ _:((A)sigma)tau+})
Definitions occuring in Statement :
partial-term-0: u[0],
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
context-subset: Gamma, phi,
face-type: 𝔽,
interval-0: 0(𝕀),
interval-type: 𝕀,
csm+: tau+,
csm-id-adjoin: [u],
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
csm-comp: G o F,
cube_set_map: A ⟶ B,
cubical_set: CubicalSet,
all: ∀x:A. B[x],
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
cubical_set: CubicalSet,
cube_set_map: A ⟶ B,
face-type: 𝔽,
context-subset: Gamma, phi,
cc-fst: p,
all: ∀x:A. B[x],
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
csm-id-adjoin: [u],
interval-0: 0(𝕀),
partial-term-0: u[0],
equal: s = t ∈ T,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
apply: f a,
csm-comp: G o F,
cube-context-adjoin: X.A,
csm+: tau+,
interval-type: 𝕀,
csm-ap-term: (t)s
FDL editor aliases :
uniform-filling-function
Latex:
uniform-filling-function\{j:l, i:l\}(Gamma;A;fill) ==
\mforall{}H,K:j\mvdash{}. \mforall{}tau:K j{}\mrightarrow{} H. \mforall{}sigma:H.\mBbbI{} j{}\mrightarrow{} Gamma. \mforall{}phi:\{H \mvdash{} \_:\mBbbF{}\}. \mforall{}u:\{H.\mBbbI{}, (phi)p \mvdash{} \_:(A)sigma\}.
\mforall{}a0:\{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][phi |{}\mrightarrow{} u[0]]\}.
((fill H sigma phi u a0)tau+ = (fill K sigma o tau+ (phi)tau (u)tau+ (a0)tau))
Date html generated:
2020_05_20-PM-04_40_48
Last ObjectModification:
2020_04_11-AM-10_53_04
Theory : cubical!type!theory
Home
Index