Nuprl Definition : fill_term
fill cA [phi ⊢→ u] a0 == comp-to-fill(Gamma.𝕀;cA) Gamma 1(Gamma.𝕀) phi u a0
Definitions occuring in Statement :
comp-to-fill: comp-to-fill(Gamma;cA),
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-id: 1(X),
apply: f a
Definitions occuring in definition :
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-id: 1(X),
comp-to-fill: comp-to-fill(Gamma;cA),
apply: f a
FDL editor aliases :
fill_term
Latex:
fill cA [phi \mvdash{}\mrightarrow{} u] a0 == comp-to-fill(Gamma.\mBbbI{};cA) Gamma 1(Gamma.\mBbbI{}) phi u a0
Date html generated:
2016_05_19-AM-10_51_48
Last ObjectModification:
2016_04_14-PM-05_28_37
Theory : cubical!type!theory
Home
Index