Definable groups
definable G spaces
o-minimal
definable G fibrations
definable G fiber bundles
Let G be a definable group, η=(E,p,X) a definable G fibration and f, h : Y → X definable G maps between definable G spaces. If f and h are definably G homotopic, then theinduced definable G fibrations f^*(η) and h^*(η) are definable G fiber homotopy equivalent.