Nuprl Definition : const-transport-fun
ConstTrans(A) == cubical-lam(G;transport-const(G.A;(cA)p;q))
Definitions occuring in Statement :
transport-const: transport-const(G;cA;a),
csm-composition: (comp)sigma,
cubical-lam: cubical-lam(X;b),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A
Definitions occuring in definition :
cubical-lam: cubical-lam(X;b),
transport-const: transport-const(G;cA;a),
cube-context-adjoin: X.A,
csm-composition: (comp)sigma,
cc-fst: p,
cc-snd: q
FDL editor aliases :
const-transport-fun
Latex:
ConstTrans(A) == cubical-lam(G;transport-const(G.A;(cA)p;q))
Date html generated:
2018_05_23-AM-10_21_27
Last ObjectModification:
2017_12_05-PM-04_28_23
Theory : cubical!type!theory
Home
Index