Nuprl Definition : equiv-bijection
equiv-bijection(e) == discrete-fun(equiv-fun(e))(⋅)
Definitions occuring in Statement :
discrete-fun: discrete-fun(f),
equiv-fun: equiv-fun(f),
cubical-term-at: u(a),
empty-fset: {},
it: ⋅
Definitions occuring in definition :
it: ⋅,
empty-fset: {},
equiv-fun: equiv-fun(f),
discrete-fun: discrete-fun(f),
cubical-term-at: u(a)
FDL editor aliases :
equiv-bijection
Latex:
equiv-bijection(e) == discrete-fun(equiv-fun(e))(\mcdot{})
Date html generated:
2017_02_21-AM-10_51_34
Last ObjectModification:
2017_02_13-AM-11_24_33
Theory : cubical!type!theory
Home
Index