Nuprl Definition : rev-type-comp
rev-type-comp(Gamma;cA) == (cA)(p;1-(q))
Definitions occuring in Statement :
csm-comp-structure: (cA)tau,
interval-rev: 1-(r),
interval-type: 𝕀,
csm-adjoin: (s;u),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A
Definitions occuring in definition :
cc-snd: q,
interval-rev: 1-(r),
cc-fst: p,
csm-adjoin: (s;u),
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-comp-structure: (cA)tau
FDL editor aliases :
rev-type-comp
Latex:
rev-type-comp(Gamma;cA) == (cA)(p;1-(q))
Date html generated:
2016_10_28-AM-07_53_03
Last ObjectModification:
2016_07_20-PM-00_41_34
Theory : cubical!type!theory
Home
Index