Nuprl Definition : filling-function
filling-function{j:l, i:l}(Gamma;A) ==
H:CubicalSet{j}
⟶ sigma:H.𝕀 j⟶ Gamma
⟶ phi:{H ⊢ _:𝔽}
⟶ u:{H.𝕀, (phi)p ⊢ _:(A)sigma}
⟶ a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
⟶ {H.𝕀 ⊢ _:(A)sigma[(phi)p |⟶ u]}
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-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,
cube_set_map: A ⟶ B,
cubical_set: CubicalSet,
function: x:A ⟶ B[x]
Definitions occuring in definition :
cubical_set: CubicalSet,
cube_set_map: A ⟶ B,
face-type: 𝔽,
cubical-term: {X ⊢ _:A},
context-subset: Gamma, phi,
function: x:A ⟶ B[x],
csm-id-adjoin: [u],
interval-0: 0(𝕀),
partial-term-0: u[0],
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
cube-context-adjoin: X.A,
interval-type: 𝕀,
csm-ap-type: (AF)s,
csm-ap-term: (t)s,
cc-fst: p
FDL editor aliases :
filling-function
Latex:
filling-function\{j:l, i:l\}(Gamma;A) ==
H:CubicalSet\{j\}
{}\mrightarrow{} sigma:H.\mBbbI{} j{}\mrightarrow{} Gamma
{}\mrightarrow{} phi:\{H \mvdash{} \_:\mBbbF{}\}
{}\mrightarrow{} u:\{H.\mBbbI{}, (phi)p \mvdash{} \_:(A)sigma\}
{}\mrightarrow{} a0:\{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][phi |{}\mrightarrow{} u[0]]\}
{}\mrightarrow{} \{H.\mBbbI{} \mvdash{} \_:(A)sigma[(phi)p |{}\mrightarrow{} u]\}
Date html generated:
2020_05_20-PM-04_40_21
Last ObjectModification:
2020_04_11-AM-10_23_57
Theory : cubical!type!theory
Home
Index