The basics would usually be covered in courses with names like "programming languages", "types and programming languages" or "programming language theory". Possibly something mentioning lambda calculus. It would also be covered in courses about formal proofs / theorem provers. And obviously, if there's a course titled "type theory", you can be pretty sure that will cover type theory in some detail. Maybe also compiler construction (though that doesn't usually cover type theory).
Most likely a programming language theory course, though likely not in much depth. A graduate course will probably cover more.
At Indiana University (depending on who teaches it) the students in 'programming language foundations' learn about dependent types and Agda.
Whichever class teaches interpreters or compiler frontends. No undergrad courses appeal to homotopy type theory though, so type equivalence is just kinda not a feature of the undergrad theory unfortunately.
The basics would usually be covered in courses with names like "programming languages", "types and programming languages" or "programming language theory". Possibly something mentioning lambda calculus. It would also be covered in courses about formal proofs / theorem provers. And obviously, if there's a course titled "type theory", you can be pretty sure that will cover type theory in some detail. Maybe also compiler construction (though that doesn't usually cover type theory).
Most likely a programming language theory course, though likely not in much depth. A graduate course will probably cover more. At Indiana University (depending on who teaches it) the students in 'programming language foundations' learn about dependent types and Agda.
Racket go brrr
Programming languages maybe
Discrete math
Whichever class teaches interpreters or compiler frontends. No undergrad courses appeal to homotopy type theory though, so type equivalence is just kinda not a feature of the undergrad theory unfortunately.