Nuprl Definition : equiv-comp
equiv-comp(H;A;E;cA;cE) == cfun-to-cop(H;Equiv(A;E);equiv_comp(H;A;E;cop-to-cfun(cA);cop-to-cfun(cE)))
Definitions occuring in Statement :
equiv_comp: equiv_comp(H;A;E;cA;cE),
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
comp-op-to-comp-fun: cop-to-cfun(cA),
cubical-equiv: Equiv(T;A)
Definitions occuring in definition :
comp-op-to-comp-fun: cop-to-cfun(cA),
equiv_comp: equiv_comp(H;A;E;cA;cE),
cubical-equiv: Equiv(T;A),
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp)
FDL editor aliases :
equiv-comp
Latex:
equiv-comp(H;A;E;cA;cE) ==
cfun-to-cop(H;Equiv(A;E);equiv\_comp(H;A;E;cop-to-cfun(cA);cop-to-cfun(cE)))
Date html generated:
2017_01_10-PM-00_10_13
Last ObjectModification:
2016_12_24-PM-00_33_06
Theory : cubical!type!theory
Home
Index