Inductive mipMapList : Set := MipMapList {
  mipMaps            : list mipMap;
  mipMapListSorted   : mipMapListIsSorted mipMaps;
  mipMapOffsetSorted : mipMapOffsetsSorted mipMaps;
}.
