タイプ・ライター その２

Advent Calendarの続きです．完全タイプのなす空間についてまとめました．
現在未完成の状態ですが，明日から仕事はじめということでいつ完成するかわからないため，とりあえず挙げておこうと思います．
追記：例として端点がない稠密な線形順序DLOを追加しました．