Nuprl Definition : fill-type-up
fill-type-up(Gamma;A;cA) == (λ(fill (cA)p+ [0(𝔽) ⟶ discr(⋅)] q)swap-interval(Gamma;(A)[0(𝕀)]))
Definitions occuring in Statement :
filling_term: fill cA [phi ⟶ u] a0,
csm-composition: (comp)sigma,
face-0: 0(𝔽),
swap-interval: swap-interval(G;A),
interval-0: 0(𝕀),
interval-type: 𝕀,
discrete-cubical-term: discr(t),
cubical-lambda: (λb),
csm+: tau+,
csm-id-adjoin: [u],
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
it: ⋅
Definitions occuring in definition :
cc-snd: q,
it: ⋅,
discrete-cubical-term: discr(t),
face-0: 0(𝔽),
cc-fst: p,
interval-type: 𝕀,
interval-0: 0(𝕀),
csm-id-adjoin: [u],
csm-ap-type: (AF)s,
cube-context-adjoin: X.A,
csm+: tau+,
csm-composition: (comp)sigma,
filling_term: fill cA [phi ⟶ u] a0,
swap-interval: swap-interval(G;A),
csm-ap-term: (t)s,
cubical-lambda: (λb)
FDL editor aliases :
fill-type-up
Latex:
fill-type-up(Gamma;A;cA) == (\mlambda{}(fill (cA)p+ [0(\mBbbF{}) \mvdash{}\mrightarrow{} discr(\mcdot{})] q)swap-interval(Gamma;(A)[0(\mBbbI{})]))
Date html generated:
2017_01_19-PM-03_05_35
Last ObjectModification:
2017_01_11-AM-10_18_06
Theory : cubical!type!theory
Home
Index