Question: what would be a good progression for a FP / Haskell programmer to internalize HoTT ideally in context of a programming language (like Agda)? Should they start studying it directly, or go through other theories (set theory, category theory, type theory, etc.) first?
Question: what would be a good progression for a FP / Haskell programmer to internalize HoTT ideally in context of a programming language (like Agda)? Should they start studying it directly, or go through other theories (set theory, category theory, type theory, etc.) first?
I’d read PLFA then Martin Escardó’s lecture notes.