Формализм для некоторых свойств из первого курса топологии

Я определю формализм (синтаксис и семантику), позволяющий очень короткими формулами выразить некоторые понятия из первого курса топологии, например компактность (хаусдорфовых пространств), связность, плотный образ, дискретность топологии, подпространство определяются при помощи формул "({a}–>{a->b})^r_{<5}^lr", "({a,b}–>{a=b})^l", "({b}–>{a->b})^l", "( –>{a})^rl" и "( –>{a})^rr" соотв.
Формализм элементарен и основан на понятиях теории категорий, конечных топологических пространств, и свойстве поднятия Квиллена из теории гомотопий.
В связи с этим формализмом возникают открытые вопросы, и я сформулирую несколько. Определяет ли формула "({a}–>{a->b})^r_{<5}^lr" компактность и для нехаусдорфовых пространств? Возникает ли нетривиальный разрешимый фрагмент элементарной топологии? Можно ли, расширив формализм, аксиоматизировать элементарную топологию, не используя теоретико-множественный язык?
Доклад основан на заметке The unreasonable power of the lifting property in elementary mathematics. A draft. http://mishap.sdf.org/by:gavrilovich/expressive_power_of_the_lifting_property.pdf