Nuprl Definition : equivU
equivU(G;E;cE) == transport(G;IdEquiv(G;(E)[0(𝕀)]))
Definitions occuring in Statement :
equiv-comp: equiv-comp(H;A;E;cA;cE),
transport: transport(Gamma;a),
csm-composition: (comp)sigma,
cubical-id-equiv: IdEquiv(X;T),
interval-0: 0(𝕀),
interval-type: 𝕀,
csm-id-adjoin: [u],
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-type: (AF)s
Definitions occuring in definition :
interval-0: 0(𝕀),
csm-id-adjoin: [u],
csm-ap-type: (AF)s,
cubical-id-equiv: IdEquiv(X;T),
csm-composition: (comp)sigma,
cc-fst: p,
interval-type: 𝕀,
cube-context-adjoin: X.A,
equiv-comp: equiv-comp(H;A;E;cA;cE),
transport: transport(Gamma;a)
FDL editor aliases :
equivU
Latex:
equivU(G;E;cE) == transport(G;IdEquiv(G;(E)[0(\mBbbI{})]))
Date html generated:
2017_01_10-PM-00_11_16
Last ObjectModification:
2017_01_06-PM-03_59_25
Theory : cubical!type!theory
Home
Index