Nuprl Definition : rev-type-line
(A)- == (A)(p;1-(q))
Definitions occuring in Statement :
interval-rev: 1-(r),
csm-adjoin: (s;u),
cc-snd: q,
cc-fst: p,
csm-ap-type: (AF)s
Definitions occuring in definition :
csm-ap-type: (AF)s,
csm-adjoin: (s;u),
cc-fst: p,
interval-rev: 1-(r),
cc-snd: q
FDL editor aliases :
rev-type-line
Latex:
(A)- == (A)(p;1-(q))
Date html generated:
2016_07_08-PM-06_52_11
Last ObjectModification:
2016_06_20-AM-11_41_52
Theory : cubical!type!theory
Home
Index