Пользователь
Prop там импредикативный. В проекте ground_zero ("Lean4 HoTT library") вместо встроенного `=` объявили свой Id который сделали `Type`. Конечно, не факт, что это эргономично, не знаю.
Id
Lean4 видели? Лучше агды в плане автоматизации (и не только). Не могу сравнить с .. rocq.
Prop там импредикативный. В проекте ground_zero ("Lean4 HoTT library") вместо встроенного `=` объявили свой
Idкоторый сделали `Type`. Конечно, не факт, что это эргономично, не знаю.Lean4 видели? Лучше агды в плане автоматизации (и не только). Не могу сравнить с .. rocq.