Формализм формализмом, но что произведение конечного числа компактов
компакт есть реально самая трудная теорема базового курса "общей топологии"
(это без метризации, гейне-бореля, хопфа-ринова и т.д.).
То есть трудность здесь весьма фундаментальная, не целиком
вытекающая из аксиомы выбора и (судя по всему)
не исчерпывается выбором формализма.

Что до локалей и/или топосов, я бы с удовольствием
посмотрел на первокурсника, которого учат таким образом.
Интересный эксперимент же, никто не пробовал.

Но если считать, что сначала мы их учим таки нормальной
топологии, то локали уже не понадобятся, ибо два курса
общей топологии - явный перебор.

Такие дела
Миша