(no subject)

Вот что у на типах данных определены произведение, сумма и возведение в степень вроде как уже все привыкли, многие уже в курсе, что и дифференцирование работает. СЯУ (на самом деле, в четверг), что вот в HoTT работает ещё и интегрирование.