Lecture
This lecture covers different kinds of maps, type operators, equivalence of types, first-class type operators, System Fw syntax and semantics, type equivalence, the calculus of constructions, pure type systems, the lambda cube, dependent types in Coq, type universes in Coq, inductive definitions and recursion in Coq, Curry-Howard correspondence, and the equivalence between LEM and DNE. It also discusses the problem with type checking in programming languages and the adoption of dependent types in Scala and Haskell.