URegina Topology and Geometry Seminar: Joseph Eremondi

Building on last week's talk, I discuss Locally Cartesian Closed Categories (LCCCs) , in which every slice category is Cartesian Closed. I describe how these categories serve model quantifiers in logic, as well as modelling type dependencies in a way not possible with simple types. I discuss how these dependent types are useful for verified programming and computer-checked proofs. To conclude, I briefly describe how different formulations of equality proofs lead to different type theories, such as Extensional Type Theory or Homotopy Type Theory.