Topology and Geometry Seminar

Location: AH 347

Speaker: Joseph Eremondi, University of Regina

Title: Locally Cartesian Closed Categories and Dependent Types

Abstract:  

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.

This event is sponsored by PIMS.