Nuprl Definition : csm-dependent
(s)dep == (s o tp{i:l};tq)
Definitions occuring in Statement :
csm-adjoin: (s;u),
typed-cc-snd: tq,
typed-cc-fst: tp{i:l},
cube-context-adjoin: X.A,
csm-ap-type: (AF)s,
csm-comp: G o F
Definitions occuring in definition :
csm-adjoin: (s;u),
csm-comp: G o F,
cube-context-adjoin: X.A,
typed-cc-fst: tp{i:l},
typed-cc-snd: tq,
csm-ap-type: (AF)s
FDL editor aliases :
csm-dependent
Latex:
(s)dep == (s o tp\{i:l\};tq)
Date html generated:
2016_07_08-PM-06_08_36
Last ObjectModification:
2016_06_27-AM-11_58_45
Theory : cubical!type!theory
Home
Index