Nuprl Definition : update-cubical-context-I
ctxt,v:I == update-context-lvl(ctxt;0;𝕀;v)
Definitions occuring in Statement :
update-context-lvl: update-context-lvl(ctxt;lvl;T;v),
interval-type: 𝕀,
natural_number: $n
Definitions occuring in definition :
update-context-lvl: update-context-lvl(ctxt;lvl;T;v),
natural_number: $n,
interval-type: 𝕀
FDL editor aliases :
update-cubical-context-I
Latex:
ctxt,v:I == update-context-lvl(ctxt;0;\mBbbI{};v)
Date html generated:
2020_05_20-PM-08_08_20
Last ObjectModification:
2020_05_04-PM-00_55_48
Theory : cubical!type!theory
Home
Index