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