Nuprl Definition : transport
transport(Gamma;a) == comp cA [0(𝔽) ⟶ discr(⋅)] a
Definitions occuring in Statement :
composition-term: comp cA [phi ⟶ u] a0,
face-0: 0(𝔽),
discrete-cubical-term: discr(t),
it: ⋅
Definitions occuring in definition :
it: ⋅,
discrete-cubical-term: discr(t),
face-0: 0(𝔽),
composition-term: comp cA [phi ⟶ u] a0
FDL editor aliases :
transport
Latex:
transport(Gamma;a) == comp cA [0(\mBbbF{}) \mvdash{}\mrightarrow{} discr(\mcdot{})] a
Date html generated:
2017_01_10-AM-09_29_13
Last ObjectModification:
2017_01_02-AM-10_32_21
Theory : cubical!type!theory
Home
Index