Nuprl Definition : csm-swap
csm-swap(G;A;B) == (p+;(q)p)
Definitions occuring in Statement :
csm+: tau+,
csm-adjoin: (s;u),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s
Definitions occuring in definition :
csm-adjoin: (s;u),
csm+: tau+,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
csm-swap
Latex:
csm-swap(G;A;B) == (p+;(q)p)
Date html generated:
2016_07_08-PM-06_08_05
Last ObjectModification:
2016_06_21-PM-01_32_33
Theory : cubical!type!theory
Home
Index