Nuprl Definition : id-fiber-center

id-fiber-center(X;T) ==  cubical-pair(q;refl(q))


Definitions occuring in Statement :  cubical-refl: refl(a),  cubical-pair: cubical-pair(u;v),  cc-snd: q,  cube-context-adjoin: X.A
Definitions occuring in definition :  cc-snd: q,  cube-context-adjoin: X.A,  cubical-refl: refl(a),  cubical-pair: cubical-pair(u;v)
FDL editor aliases :  id-fiber-center
Latex:
id-fiber-center(X;T)  ==    cubical-pair(q;refl(q))


Date html generated: 2017_01_10-AM-09_00_22
Last ObjectModification: 2016_12_14-PM-03_04_47

Theory : cubical!type!theory


Home Index