Nuprl Definition : cubical-id-is-equiv
cubical-id-is-equiv(X;T) == (λcontr-witness(X.T; id-fiber-center(X;T); id-fiber-contraction(X;T)))
Definitions occuring in Statement :
id-fiber-contraction: id-fiber-contraction(X;T),
id-fiber-center: id-fiber-center(X;T),
contr-witness: contr-witness(X; c; p),
cubical-lambda: (λb),
cube-context-adjoin: X.A
Definitions occuring in definition :
id-fiber-contraction: id-fiber-contraction(X;T),
id-fiber-center: id-fiber-center(X;T),
cube-context-adjoin: X.A,
contr-witness: contr-witness(X; c; p),
cubical-lambda: (λb)
FDL editor aliases :
cubical-id-is-equiv
Latex:
cubical-id-is-equiv(X;T) == (\mlambda{}contr-witness(X.T; id-fiber-center(X;T); id-fiber-contraction(X;T)))
Date html generated:
2017_01_10-AM-09_03_37
Last ObjectModification:
2016_12_14-PM-03_07_00
Theory : cubical!type!theory
Home
Index