Nuprl Definition : fill-type-down
fill-type-down(Gamma;A;cA) == (fill-type-up(Gamma;(A)-;csm-composition((p;1-(q));cA)))(p;1-(q))
Definitions occuring in Statement :
fill-type-up: fill-type-up(Gamma;A;cA),
rev-type-line: (A)-,
csm-composition: csm-composition(sigma;comp),
interval-rev: 1-(r),
csm-adjoin: (s;u),
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s
Definitions occuring in definition :
csm-ap-term: (t)s,
fill-type-up: fill-type-up(Gamma;A;cA),
rev-type-line: (A)-,
csm-composition: csm-composition(sigma;comp),
csm-adjoin: (s;u),
cc-fst: p,
interval-rev: 1-(r),
cc-snd: q
FDL editor aliases :
fill-type-down
Latex:
fill-type-down(Gamma;A;cA) == (fill-type-up(Gamma;(A)-;csm-composition((p;1-(q));cA)))(p;1-(q))
Date html generated:
2016_07_08-PM-07_16_15
Last ObjectModification:
2016_06_21-PM-05_29_26
Theory : cubical!type!theory
Home
Index