Просто хотел поделиться противоположным "острым ощущением" (С), что например, на этом форуме максимум пара человек может утверждать, что понимают эту формулу.
Хм, странно. У меня есть несколько мыслей насчёт этого.
1. Дальше вы приводите цитаты из гомотопической теории типов, но это не единственная теория, в языке которой есть равенство. Есть всевозможные расширения λ-исчисления (или сужения — например, одни только комбинаторы, свойства которых придётся описывать для каждого своей аксиомой), есть теории первого порядка с равенством (ну и второго). Там везде о равенстве говорят довольно разные (из-за разных средств выражения) наборы аксиом, но все они объединены одной идеей: если две вещи равны, подстановка одной вместо другой никогда ничего не меняет; и очень часто другой идеей (экстенсиональность): если две вещи нельзя отличить всеми доступными средствами, они равны.
2. Эти идеи можно понять, не имея знакомства с конкретными формальными теориями и аппаратом матлогики вообще. Иногда может быть достаточно того введения, которое обычно есть в учебниках матанализа.
3. Ergo, я не думаю, что пара. На порядка два—два с половиной больше среди довольно активных участников, и неизвестно на сколько среди всех.
-- Чт мар 17, 2016 12:26:43 --4. Можно с уверенностью утверждать, что математика о равенстве знает* уже (и уже давно) всё. Так что не буду ничего говорить о том, что по последней ссылке, но, если там есть претензии на новизну, они наверняка зря.
-- Чт мар 17, 2016 12:27:39 --Вот, тут как раз о том, чем отличаются
и
(см. выше в теме).
Тем, что это разные термы. Это банально.