Joint Los Angeles Topology Seminar

UCLA, Room 4645 in the Geology Building

When considering topological spaces with algebraic structures, there are certain properties which are invariant under homotopy equivalence, such as homotopy-associativity, and others that are not, such as strict associativity. A natural question is: which properties, in general, are homotopy invariant? As this involves a general notion of "property", it is a question of mathematical logic, and in particular suggests that we need a system of logical notation which is somehow well-adapted to the homotopical context. Such a system was introduced by Voevodsky under the name Homotopy Type Theory. I will discuss a sort of toy version of this, which is the case of "first-order homotopical logic", in which we can very thoroughly work out this question of homotopy-invariance. The proof of the resulting homotopy-invariance theorem involves some interesting ("fibrational") structures coming from categorical logic.