Abstract: Type system plays an important role in the research of the foundations of programming language. In particular, the polymorphic type systems with subtyping capture the key concepts of object-oriented programming language such as subtyping and polymorphism. A polymorphic type system with higher-order subtyping, which is called the type system λω×\-≤, is investigated. By using the inserters and the theory of fibrations, a kind of fibration called the λω×\-≤ fibration is introduced as the semantic model of the type system λω×\-≤. In this paper, the equation theory of the type system λω×\-≤, especially, the equations related to the bounded quantification type, are discussed. Furthermore, by using the properties of the inserters, the semantic soundness of the λω×\-≤ fibration with respect to the equation theory of the type system λω×\-≤ is shown.