Nuprl Definition : rev-transport-fun
rev-transport-fun(Gamma;A;cA) == transport-fun(Gamma;(A)-;csm-composition((p;1-(q));cA))
Definitions occuring in Statement :
transport-fun: transport-fun(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
Definitions occuring in definition :
transport-fun: transport-fun(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 :
rev-transport-fun
Latex:
rev-transport-fun(Gamma;A;cA) == transport-fun(Gamma;(A)-;csm-composition((p;1-(q));cA))
Date html generated:
2016_07_08-PM-06_53_22
Last ObjectModification:
2016_06_20-PM-00_06_49
Theory : cubical!type!theory
Home
Index