Nuprl Definition : transEquiv-trans
transEquivFun(p) == equiv-fun(transEquiv{i:l}(G;A;p))
Definitions occuring in Statement :
transEquiv: transEquiv{i:l}(G;A;p),
equiv-fun: equiv-fun(f)
Definitions occuring in definition :
equiv-fun: equiv-fun(f),
transEquiv: transEquiv{i:l}(G;A;p)
FDL editor aliases :
transEquiv-trans
Latex:
transEquivFun(p) == equiv-fun(transEquiv\{i:l\}(G;A;p))
Date html generated:
2018_05_23-PM-06_11_50
Last ObjectModification:
2017_11_24-AM-09_40_12
Theory : cubical!type!theory
Home
Index