Representatives from Fields Information Security will present on their Information Security Specialist Program. Email cschul3@uwo.ca for more information and program brochure.

Homotopy type theory (HoTT) is a formal system that allows us to do homotopy-invariant mathematics in a natural way, where types can be seen as representing topological spaces. In HoTT, every type has types of paths (identity types) between its terms, paths between paths, etc., giving types a higher groupoidal structure. Simplicial type theory is an extension of HoTT that adds extra categorical structure to types using constructions similar to those in simplicial sets, making it possible to state a definition of an infinity-category that does not depend on a particular set-theoretic model. Additionally, using type-theoretic foundations makes it easier to formalise parts of the theory of infinity-categories in proof assistants, and in particular the Rzk proof assistant developed specifically for this type theory. We present an introduction to HoTT and simplicial type theory, and discuss possible directions one can consider in synthetic higher category theory.