Nuprl Definition : transport-fun
transport-fun(Gamma;A;cA) == (λtransport(Gamma.(A)[0(𝕀)];csm-composition(p+;cA);q))
Definitions occuring in Statement :
transport: transport(Gamma;cA;a),
csm-composition: csm-composition(sigma;comp),
interval-0: 0(𝕀),
interval-type: 𝕀,
cubical-lambda: (λb),
csm+: tau+,
csm-id-adjoin: [u],
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-type: (AF)s
Definitions occuring in definition :
cc-snd: q,
cc-fst: p,
interval-type: 𝕀,
interval-0: 0(𝕀),
csm-id-adjoin: [u],
csm-ap-type: (AF)s,
cube-context-adjoin: X.A,
csm+: tau+,
csm-composition: csm-composition(sigma;comp),
transport: transport(Gamma;cA;a),
cubical-lambda: (λb)
FDL editor aliases :
transport-fun
Latex:
transport-fun(Gamma;A;cA) == (\mlambda{}transport(Gamma.(A)[0(\mBbbI{})];csm-composition(p+;cA);q))
Date html generated:
2016_06_16-PM-06_38_55
Last ObjectModification:
2016_06_16-PM-03_59_25
Theory : cubical!type!theory
Home
Index