TaPL в процессе, есть что-нибудь ещё?
Желательно вместе с примерами на каком-нибудь Coq/Agda/etc
И ещё, что нужно вкуривать перед HoTT?
agda, coq, idris, теория типов
TaPL в процессе, есть что-нибудь ещё?
Желательно вместе с примерами на каком-нибудь Coq/Agda/etc
И ещё, что нужно вкуривать перед HoTT?