Flower Hour

Speaker: (Western)

"Mathematical Biology Seminar"

Time: 11:00

Room: WSC 187

Geometry and Combinatorics

Speaker: (Western)

"no talk this week"

Time: 15:30

Room: MC 108

Public Lecture

Speaker: Aaron Crighton (Fields Institute)

"Fields Quantitative Information Security Specialist Program"

Time: 15:30

Room: MC 107

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

Transformation Groups Seminar

Speaker: Vladimir Gorchakov (Western)

"Cohomology of Free Loop Spaces III"

Time: 09:30

Room: MC 108

Graduate Seminar

Speaker: Theofanis Chatzidiamantis Christoforidis (Western)

"Formalising higher category theory"

Time: 15:30

Room: MC 107

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.