Abstract: In recent years, peoples have studied many type systems, and the type systems with high order subtyping play an important role in the research of formal foundation of object oriented technology. But the researchers have not yet got the perfect semantic model for high order subtyping. λω × ≤ fibration can be regarded as the categorical semantic model of high order subtyping. Its base category is the special enriched order category with inserter, and its fibre category is the Cartesian closed category with coercion structure.