Insights from the LMS Hardy Lectureship 2025 at Cardiff University

This year's Hardy Lecturer, Professor Emily Riehl visited Cardiff University as part of the LMS Hardy Lectureship Tour. Dr John Harvey reflects on the event.

The HoTTest day of the year.

CP Snow recounted how GH Hardy would work from nine to one on mathematics before retiring to the cricket pitch for the afternoon. The hot afternoon of 27 June was not one for lazing around in the sun at the School of Mathematics. The ground floor teemed with open day visitors, while upstairs Professor Emly Riehl, this year’s LMS Hardy Lecturer, inspired as a girl by Hardy’s poetic description of mathematics as well as his admirable work-life balance, faced an excited crowd ranging from undergraduates to senior professors to expound on “Homotopy types as homotopy types”.

Riehl arrived to us from a foreign land – not just from Johns Hopkins University in Baltimore, but from an entirely alternative set of mathematical foundations. Homotopy type theory (often abbreviated as HoTT) builds mathematics on a foundation of types rather than sets, with abstract homotopy theory being used to understand these types. The first “homotopy types” in the cryptic title, Riehl eventually confessed, referred to the objects of homotopy type theory. We were to be introduced to these through the more traditional “homotopy types” of topology. Of all the talks Riehl would deliver on her tour through the UK, this one, we were assured, was the wackiest.

In the category of simplicial sets, the Kan complexes, the fibrant objects which are so fundamental in homotopy theory, were recast as “spaces”. Fibrations became “families of spaces”. For a space A, the central space for this talk was to be the path space of A, but in a simplicial way – the set of maps from the standard 1-simplex into A.

The principle of “path induction” from homotopy type theory, Riehl explained, was that, for a family of spaces over a path space, any section defined on the constant paths could be extended to a section on the entire path space. Not only this – if a second family were to be defined over the first family, then a section of this second family could always be given from a section defined over the pre-image in the first family of the constant paths. It was left to the audience’s imagination whether this might go all the way up.

This principle was then put to work to demonstrate that paths could always be concatenated. Some claimed this was trivial – just rescale the two component paths and join their domain. Ah, said Prof Riehl, that might work, but a simplicial path has no parameter, it cannot be rescaled. Others claimed it was impossible. You might think so, but the trick is to only consider Kan complexes. Both camps were wowed as Prof Riehl performed the concatenation before their eyes (see picture).

Our neighbour Professor Grigory Garkusha, from Swansea University, joined us earlier in the afternoon to provide a fine historical overview of the links between homotopy theory and algebraic geometry. The undergraduate students in attendance were excited to see the cutting edge of mathematics in operation, as well as to see their usually so wise lecturers looking confused for a change, while recent PhD graduate, Dr Sam Hannah, announced he was heading straight to the library to learn as much homotopy type theory as he could.

The School’s thanks are due to Dr Simon Wood, who put much work into organising this event but sadly could not attend, to Dr Ulrich Pennig, who prepared the audience in the morning with an introduction to simplicial sets, to Prof Roger Behrend for playing host and to Naomi Wray, who drummed up an audience, chased down the caterers and polished the chalkboards to a Germanic precision so that Riehl’s commutative diagrams might unfold with a visual grace that matched their intellectual origins.

Had Riehl found the mathematical life as pleasant as Hardy? Yes – she played cricket during her year at Cambridge. All work and no play never ends well. We waved her goodbye as she headed off to the Bannau Brycheiniog for the weekend before the grind of the tour started again.