We describe an extension of Martin-Lof's type theory with dependent record types and subtyping and use it for obtaining a formal definition of a general structure of the algorithms of sorting by insertion. We start by giving a general formulation of the sorting problem according to which the most general sorting algorithms are those that can be used for ordering lists over any set, along any total relation on the set. In particular, the best known members of the family of algorithms of sorting by insertion, namely straight insertion sort and tree sort, are of this kind. The proposed structure of the algorithms of sorting by insertion is based upon a specification of an abstract data type, which we call of insertion structures. The general method of sorting by insertion is then written as a program depending on unspecified implementation of insertion structures. We therefore call it abstract insertion sort. The concrete algorithms of sorting by insertion correspond to particular implementations of insertion structures. We discuss how it is possible to peecify the operations on insertion structures so as to accurately describe the intended family of algorithms. We also derive axioms for the insertion structures so as to obtain a natural decomposition into lemmas of the proofs of correctness of the algorithms of the family.