Nuprl Definition : cubical-id-equiv
IdEquiv(X;T) == equiv-witness(cubical-id-fun(X);cubical-id-is-equiv(X;T))
Definitions occuring in Statement :
cubical-id-is-equiv: cubical-id-is-equiv(X;T),
equiv-witness: equiv-witness(f;cntr),
cubical-id-fun: cubical-id-fun(X)
Definitions occuring in definition :
cubical-id-is-equiv: cubical-id-is-equiv(X;T),
cubical-id-fun: cubical-id-fun(X),
equiv-witness: equiv-witness(f;cntr)
FDL editor aliases :
cubical-id-equiv
Latex:
IdEquiv(X;T) == equiv-witness(cubical-id-fun(X);cubical-id-is-equiv(X;T))
Date html generated:
2017_01_10-AM-09_05_47
Last ObjectModification:
2016_12_14-PM-02_25_25
Theory : cubical!type!theory
Home
Index