3 ms·
That has more to do with type theory directly. So far the lectures have been a great intro to constructive logics which while build to type theory and dependent
by tel 13y ago
That has more to do with type theory directly. So far the lectures have been a great intro to constructive logics which while build to type theory and dependently typed languages, but that's not necessarily the thrust of HoTT.