Nuprl Definition : transprt-fun
transprt-fun(Gamma;A;cA) == (λtransprt(Gamma.(A)[0(𝕀)];(cA)p+;q))
Definitions occuring in Statement :
transprt: transprt(G;cA;a0),
csm-comp-structure: (cA)tau,
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-comp-structure: (cA)tau,
transprt: transprt(G;cA;a0),
cubical-lambda: (λb)
FDL editor aliases :
transprt-fun
Latex:
transprt-fun(Gamma;A;cA) == (\mlambda{}transprt(Gamma.(A)[0(\mBbbI{})];(cA)p+;q))
Date html generated:
2017_01_10-AM-09_45_37
Last ObjectModification:
2017_01_02-PM-01_00_35
Theory : cubical!type!theory
Home
Index