I am working on categorical model for higher-order subtyping. I hope someone can tell me where can I find the books or papers about insertor in enriched categories. Thanks very much!