I developed The HoTT Game, which is a game in Cubial Agda where mathematicians can try out Homotopy Type Theory using agda.