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

progressionfor 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.