именно, одноточечная

@dluciv спасибо

@jtootf Занимается же кто-то делом... Аж зависть берёт.

@dluciv да это наоборот. надо - пробовать описывать на Agda индексированные категории, а получается - читать в интернете всякое с картинками

@matimatik Это когда к топологическому пространству добавляют точку на бесконечности, чтобы сделать его компактным. http://en.wikipedia.org/wiki/One-point_compactification