Nuprl Definition : update-context4
update-context4{i:l}(X;phi) == bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;phi))
Definitions occuring in Statement :
restrict-cubical-context: restrict-cubical-context{i:l}(ctxt;trm),
bind-provision: bind-provision(x;t.f[t])
Definitions occuring in definition :
bind-provision: Error :bind-provision,
restrict-cubical-context: restrict-cubical-context{i:l}(ctxt;trm)
FDL editor aliases :
update-context4
Latex:
update-context4\{i:l\}(X;phi) == bind-provision(X;ctxt.restrict-cubical-context\{i:l\}(ctxt;phi))
Date html generated:
2020_05_20-PM-08_14_42
Last ObjectModification:
2020_05_11-AM-10_15_38
Theory : cubical!type!theory
Home
Index